1 /-
2 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl
5
6 Theory of complete lattices.
7 -/
8 import order.bounded_lattice order.bounds data.set.basic tactic.pi_instances
src └───────────────────┘ └──────────┘ └────────────┘ └─────────────────┘
9
10 set_option old_structure_cmd true
doc └───────────────┘
11 open set
12
13 namespace lattice
14 universes u v w w₂
15 variables {α : Type u} {β : Type v} {ι : Sort w} {ι₂ : Sort w₂}
16
17 /-- class for the `Sup` operator -/
18 class has_Sup (α : Type u) := (Sup : set α → α)
id └──┘ └─┘ ┴ ┴ ┴
src └─┘
typ └──┘ └─┘ ┴ ┴ ┴
19 /-- class for the `Inf` operator -/
20 class has_Inf (α : Type u) := (Inf : set α → α)
id └──┘ └─┘ ┴ ┴ ┴
src └─┘
typ └──┘ └─┘ ┴ ┴ ┴
21 /-- Supremum of a set -/
22 def Sup [has_Sup α] : set α → α := has_Sup.Sup
id └─────┘ ┴ └─┘ ┴ ┴ └─────────┘
src └─────┘ └─┘ └─────────┘
typ └─────┘ ┴ └─┘ ┴ ┴ └─────────┘
doc └─────┘
23 /-- Infimum of a set -/
24 def Inf [has_Inf α] : set α → α := has_Inf.Inf
id └─────┘ ┴ └─┘ ┴ ┴ └─────────┘
src └─────┘ └─┘ └─────────┘
typ └─────┘ ┴ └─┘ ┴ ┴ └─────────┘
doc └─────┘
25 /-- Indexed supremum -/
26 def supr [has_Sup α] (s : ι → α) : α := Sup (range s)
id └─────┘ ┴ ┴ ┴ ┴ └─┘ └───┘ ┴
src └─────┘ └─┘ └───┘
typ └─────┘ ┴ ┴ ┴ ┴ └─┘ └───┘ ┴
doc └─────┘ └─┘ └───┘
27 /-- Indexed infimum -/
28 def infi [has_Inf α] (s : ι → α) : α := Inf (range s)
id └─────┘ ┴ ┴ ┴ ┴ └─┘ └───┘ ┴
src └─────┘ └─┘ └───┘
typ └─────┘ ┴ ┴ ┴ ┴ └─┘ └───┘ ┴
doc └─────┘ └─┘ └───┘
29
30 lemma has_Inf_to_nonempty (α) [has_Inf α] : nonempty α := ⟨Inf ∅⟩
id └─────┘ ┴ └──────┘ ┴ └─┘ ┴
src └─────┘ └──────┘ └─┘ ┴
typ └─────┘ ┴ └──────┘ ┴ └─┘ ┴
doc └─────┘ └─┘
31 lemma has_Sup_to_nonempty (α) [has_Sup α] : nonempty α := ⟨Sup ∅⟩
id └─────┘ ┴ └──────┘ ┴ └─┘ ┴
src └─────┘ └──────┘ └─┘ ┴
typ └─────┘ ┴ └──────┘ ┴ └─┘ ┴
doc └─────┘ └─┘
32
33 notation `⨆` binders `, ` r:(scoped f, supr f) := r
id └──┘
src └──┘
typ └──┘
doc └──┘
34 notation `⨅` binders `, ` r:(scoped f, infi f) := r
id └──┘
src └──┘
typ └──┘
doc └──┘
35
36 section prio
37 set_option default_priority 100 -- see Note [default priority]
doc └──────────────┘
38 /-- A complete lattice is a bounded lattice which
39 has suprema and infima for every subset. -/
40 class complete_lattice (α : Type u) extends bounded_lattice α, has_Sup α, has_Inf α :=
id ┴ └──┘ └─────────────┘ ┴ └─────┘ ┴ └─────┘ ┴
src └─────────────┘ └─────┘ └─────┘
typ ┴ └──┘ └─────────────┘ ┴ └─────┘ ┴ └─────┘ ┴
doc └─────────────┘ └─────┘ └─────┘
41 (le_Sup : ∀s, ∀a∈s, a ≤ Sup s)
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
42 (Sup_le : ∀s a, (∀b∈s, b ≤ a) → Sup s ≤ a)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
43 (Inf_le : ∀s, ∀a∈s, Inf s ≤ a)
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
44 (le_Inf : ∀s a, (∀b∈s, a ≤ b) → a ≤ Inf s)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
45
46 /-- A complete linear order is a linear order whose lattice structure is complete. -/
47 class complete_linear_order (α : Type u) extends complete_lattice α, decidable_linear_order α
id ┴ └──┘ └──────────────┘ ┴ └────────────────────┘ ┴
src └──────────────┘ └────────────────────┘
typ ┴ └──┘ └──────────────┘ ┴ └────────────────────┘ ┴
doc └──────────────┘
48 end prio
49
50 section
51 variables [complete_lattice α] {s t : set α} {a b : α}
id └──────────────┘ └─┘
src └──────────────┘ └─┘
typ └──────────────┘ └─┘
doc └──────────────┘
52
53 @[ematch] theorem le_Sup : a ∈ s → a ≤ Sup s := complete_lattice.le_Sup s a
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─────────────────────┘ ┴ ┴
src └────┘ ┴ ┴ └─┘ └─────────────────────┘
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─────────────────────┘ ┴ ┴
doc └────┘ └─┘
54
55 theorem Sup_le : (∀b∈s, b ≤ a) → Sup s ≤ a := complete_lattice.Sup_le s a
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────────────────────┘ ┴ ┴
src ┴ └─┘ ┴ └─────────────────────┘
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────────────────────┘ ┴ ┴
doc └─┘
56
57 @[ematch] theorem Inf_le : a ∈ s → Inf s ≤ a := complete_lattice.Inf_le s a
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────────────────────┘ ┴ ┴
src └────┘ ┴ └─┘ ┴ └─────────────────────┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────────────────────┘ ┴ ┴
doc └────┘ └─┘
58
59 theorem le_Inf : (∀b∈s, a ≤ b) → a ≤ Inf s := complete_lattice.le_Inf s a
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─────────────────────┘ ┴ ┴
src ┴ ┴ └─┘ └─────────────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─────────────────────┘ ┴ ┴
doc └─┘
60
61 lemma is_lub_Sup : is_lub s (Sup s) := ⟨assume x, le_Sup, assume x, Sup_le⟩
id └────┘ ┴ └─┘ ┴ ┴ └────┘ ┴ └────┘
src └────┘ └─┘ └────┘ └────┘
typ └────┘ ┴ └─┘ ┴ ┴ └────┘ ┴ └────┘
doc └────┘ └─┘
62
63 lemma is_lub_iff_Sup_eq : is_lub s a ↔ Sup s = a := is_lub_iff_eq_of_is_lub is_lub_Sup
id └────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────────────────────┘ └────────┘
src └────┘ ┴ └─┘ ┴ └─────────────────────┘ └────────┘
typ └────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────────────────────┘ └────────┘
doc └────┘ └─┘
64
65 lemma is_glb_Inf : is_glb s (Inf s) := ⟨assume a, Inf_le, assume a, le_Inf⟩
id └────┘ ┴ └─┘ ┴ ┴ └────┘ ┴ └────┘
src └────┘ └─┘ └────┘ └────┘
typ └────┘ ┴ └─┘ ┴ ┴ └────┘ ┴ └────┘
doc └────┘ └─┘
66
67 lemma is_glb_iff_Inf_eq : is_glb s a ↔ Inf s = a := is_glb_iff_eq_of_is_glb is_glb_Inf
id └────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────────────────────┘ └────────┘
src └────┘ ┴ └─┘ ┴ └─────────────────────┘ └────────┘
typ └────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────────────────────┘ └────────┘
doc └────┘ └─┘
68
69 theorem le_Sup_of_le (hb : b ∈ s) (h : a ≤ b) : a ≤ Sup s :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
doc └─┘
70 le_trans h (le_Sup hb)
id └──────┘ ┴ └────┘ └┘
src └──────┘ └────┘
typ └──────┘ ┴ └────┘ └┘
71
72 theorem Inf_le_of_le (hb : b ∈ s) (h : b ≤ a) : Inf s ≤ a :=
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘
73 le_trans (Inf_le hb) h
id └──────┘ └────┘ └┘ ┴
src └──────┘ └────┘
typ └──────┘ └────┘ └┘ ┴
74
75 theorem Sup_le_Sup (h : s ⊆ t) : Sup s ≤ Sup t :=
id ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src ┴ └─┘ ┴ └─┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘
76 Sup_le (assume a, assume ha : a ∈ s, le_Sup $ h ha)
id └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ └┘
src └────┘ ┴ └────┘
typ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ └┘
77
78 theorem Inf_le_Inf (h : s ⊆ t) : Inf t ≤ Inf s :=
id ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src ┴ └─┘ ┴ └─┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘
79 le_Inf (assume a, assume ha : a ∈ s, Inf_le $ h ha)
id └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ └┘
src └────┘ ┴ └────┘
typ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ └┘
80
81 @[simp] theorem Sup_le_iff : Sup s ≤ a ↔ (∀b ∈ s, b ≤ a) :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─┘
82 ⟨assume : Sup s ≤ a, assume b, assume : b ∈ s,
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
83 le_trans (le_Sup ‹b ∈ s›) ‹Sup s ≤ a›,
id └──────┘ └────┘ ┴┴ ┴ ┴┴ ┴└─┘ ┴ ┴ ┴┴
src └──────┘ └────┘ ┴ ┴ ┴ ┴└─┘ ┴ ┴
typ └──────┘ └────┘ ┴┴ ┴ ┴┴ ┴└─┘ ┴ ┴ ┴┴
doc ┴ ┴ ┴└─┘ ┴
84 Sup_le⟩
id └────┘
src └────┘
typ └────┘
85
86 @[simp] theorem le_Inf_iff : a ≤ Inf s ↔ (∀b ∈ s, a ≤ b) :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─┘
87 ⟨assume : a ≤ Inf s, assume b, assume : b ∈ s,
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
doc └─┘
88 le_trans ‹a ≤ Inf s› (Inf_le ‹b ∈ s›),
id └──────┘ ┴┴ ┴ └─┘ ┴┴ └────┘ ┴┴ ┴ ┴┴
src └──────┘ ┴ ┴ └─┘ ┴ └────┘ ┴ ┴ ┴
typ └──────┘ ┴┴ ┴ └─┘ ┴┴ └────┘ ┴┴ ┴ ┴┴
doc ┴ └─┘ ┴ ┴ ┴
89 le_Inf⟩
id └────┘
src └────┘
typ └────┘
90
91 -- how to state this? instead a parameter `a`, use `∃a, a ∈ s` or `s ≠ ∅`?
92 theorem Inf_le_Sup (h : a ∈ s) : Inf s ≤ Sup s :=
id ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src ┴ └─┘ ┴ └─┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘
93 by have := le_Sup h; finish
id └────┘ ┴
src └──────┘└────┘┴ └──────
typ └──────┘└────┘┴┴ └──────
doc └──────┘ ┴ └──────
txt └──────┘ ┴ └──────
par └──────┘ ┴ └──────
pid └───┘└─┘ ┴ └
st └─────────────────────────
94 --Inf_le_of_le h (le_Sup h)
src ────────────────────────────
typ ────────────────────────────
doc ────────────────────────────
txt ────────────────────────────
par ────────────────────────────
pid ────────────────────────────
st ────────────────────────────
95
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
96 -- TODO: it is weird that we have to add union_def
src ──────────────────────────────────────────────────┘
typ ──────────────────────────────────────────────────┘
doc ──────────────────────────────────────────────────┘
txt ──────────────────────────────────────────────────┘
par ──────────────────────────────────────────────────┘
pid ──────────────────────────────────────────────────┘
st ──────────────────────────────────────────────────┘
97 theorem Sup_union {s t : set α} : Sup (s ∪ t) = Sup s ⊔ Sup t :=
id └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘ └─┘
98 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
99 (by finish)
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st └─────┘
100 (sup_le (Sup_le_Sup $ subset_union_left _ _) (Sup_le_Sup $ subset_union_right _ _))
id └────┘ └────────┘ └───────────────┘ └────────┘ └────────────────┘
src └────┘ └────────┘ └───────────────┘ └────────┘ └────────────────┘
typ └────┘ └────────┘ └───────────────┘ └────────┘ └────────────────┘
101
102 /- old proof:
103 le_antisymm
104 (Sup_le $ assume a h, or.rec_on h (le_sup_left_of_le ∘ le_Sup) (le_sup_right_of_le ∘ le_Sup))
105 (sup_le (Sup_le_Sup $ subset_union_left _ _) (Sup_le_Sup $ subset_union_right _ _))
106 -/
107
108 theorem Sup_inter_le {s t : set α} : Sup (s ∩ t) ≤ Sup s ⊓ Sup t :=
id └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘ └─┘
109 by finish
src └──────
typ └──────
doc └──────
txt └──────
par └──────
pid └
st └───────
110 /-
src ───
typ ───
doc ───
txt ───
par ───
pid ───
st ───
111 Sup_le (assume a ⟨a_s, a_t⟩, le_inf (le_Sup a_s) (le_Sup a_t))
src ─────────────────────────────────────────────────────────────────
typ ─────────────────────────────────────────────────────────────────
doc ─────────────────────────────────────────────────────────────────
txt ─────────────────────────────────────────────────────────────────
par ─────────────────────────────────────────────────────────────────
pid ─────────────────────────────────────────────────────────────────
st ─────────────────────────────────────────────────────────────────
112 -/
src ───
typ ───
doc ───
txt ───
par ───
pid ───
st ───
113
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
114 theorem Inf_union {s t : set α} : Inf (s ∪ t) = Inf s ⊓ Inf t :=
id └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └─┘ └─┘ └─┘
115 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
116 (le_inf (Inf_le_Inf $ subset_union_left _ _) (Inf_le_Inf $ subset_union_right _ _))
id └────┘ └────────┘ └───────────────┘ └────────┘ └────────────────┘
src └────┘ └────────┘ └───────────────┘ └────────┘ └────────────────┘
typ └────┘ └────────┘ └───────────────┘ └────────┘ └────────────────┘
117 (by finish)
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st └─────┘
118
119 /- old proof:
120 le_antisymm
121 (le_inf (Inf_le_Inf $ subset_union_left _ _) (Inf_le_Inf $ subset_union_right _ _))
122 (le_Inf $ assume a h, or.rec_on h (inf_le_left_of_le ∘ Inf_le) (inf_le_right_of_le ∘ Inf_le))
123 -/
124
125 theorem le_Inf_inter {s t : set α} : Inf s ⊔ Inf t ≤ Inf (s ∩ t) :=
id └─┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
src └─┘ └─┘ ┴ └─┘ ┴ └─┘ ┴
typ └─┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘ └─┘ └─┘
126 by finish
src └──────
typ └──────
doc └──────
txt └──────
par └──────
pid └
st └───────
127 /-
src ───
typ ───
doc ───
txt ───
par ───
pid ───
st ───
128 le_Inf (assume a ⟨a_s, a_t⟩, sup_le (Inf_le a_s) (Inf_le a_t))
src ───────────────────────────────────────────────────────────────
typ ───────────────────────────────────────────────────────────────
doc ───────────────────────────────────────────────────────────────
txt ───────────────────────────────────────────────────────────────
par ───────────────────────────────────────────────────────────────
pid ───────────────────────────────────────────────────────────────
st ───────────────────────────────────────────────────────────────
129 -/
src ───
typ ───
doc ───
txt ───
par ───
pid ───
st ───
130
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
131 @[simp] theorem Sup_empty : Sup ∅ = (⊥ : α) :=
id └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴
doc └──┘ └─┘
132 le_antisymm (by finish) (by finish)
id └─────────┘
src └─────────┘ └────┘ └────┘
typ └─────────┘ └────┘ └────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
st └─────┘ └─────┘
133 -- le_antisymm (Sup_le (assume _, false.elim)) bot_le
134
135 @[simp] theorem Inf_empty : Inf ∅ = (⊤ : α) :=
id └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴
doc └──┘ └─┘
136 le_antisymm (by finish) (by finish)
id └─────────┘
src └─────────┘ └────┘ └────┘
typ └─────────┘ └────┘ └────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
st └─────┘ └─────┘
137 --le_antisymm le_top (le_Inf (assume _, false.elim))
138
139 @[simp] theorem Sup_univ : Sup univ = (⊤ : α) :=
id └─┘ └──┘ ┴ ┴ ┴
src └─┘ └──┘ ┴ ┴
typ └─┘ └──┘ ┴ ┴ ┴
doc └──┘ └─┘
140 le_antisymm (by finish) (le_Sup ⟨⟩) -- finish fails because ⊤ ≤ a simplifies to a = ⊤
id └─────────┘ └────┘ ┴
src └─────────┘ └────┘ └────┘ ┴
typ └─────────┘ └────┘ └────┘ ┴
doc └────┘
txt └────┘
par └────┘
st └─────┘
141 --le_antisymm le_top (le_Sup ⟨⟩)
142
143 @[simp] theorem Inf_univ : Inf univ = (⊥ : α) :=
id └─┘ └──┘ ┴ ┴ ┴
src └─┘ └──┘ ┴ ┴
typ └─┘ └──┘ ┴ ┴ ┴
doc └──┘ └─┘
144 le_antisymm (Inf_le ⟨⟩) bot_le
id └─────────┘ └────┘ ┴ └────┘
src └─────────┘ └────┘ ┴ └────┘
typ └─────────┘ └────┘ ┴ └────┘
145
146 -- TODO(Jeremy): get this automatically
147 @[simp] theorem Sup_insert {a : α} {s : set α} : Sup (insert a s) = a ⊔ Sup s :=
id ┴ └─┘ ┴ └─┘ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └─┘ └─┘ └────┘ ┴ ┴ └─┘
typ ┴ └─┘ ┴ └─┘ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
doc └──┘ └─┘ └─┘
148 have Sup {b | b = a} = a,
id └─┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
149 from le_antisymm (Sup_le $ assume b b_eq, b_eq ▸ le_refl _) (le_Sup rfl),
id └─────────┘ └────┘ ┴ └──┘ └──┘ ┴ └─────┘ └────┘ └─┘
src └─────────┘ └────┘ ┴ └─────┘ └────┘ └─┘
typ └─────────┘ └────┘ ┴ └──┘ └──┘ ┴ └─────┘ └────┘ └─┘
150 calc Sup (insert a s) = Sup {b | b = a} ⊔ Sup s : Sup_union
id └─┘ └────┘ ┴ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ └───────┘
src └─┘ └────┘ └─┘ ┴ ┴ ┴ └─┘ └───────┘
typ └─┘ └────┘ ┴ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ └───────┘
doc └─┘ └─┘ └─┘
151 ... = a ⊔ Sup s : by rw [this]
id ┴ ┴ └─┘ ┴ └──┘
src ┴ └─┘ └──┘ └─
typ ┴ ┴ └─┘ ┴ └──┘└──┘└─
doc └─┘ └──┘ └─
txt └──┘ └─
par └──┘ └─
pid └┘ ┴└
st └───────┘┴└
152
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
153 @[simp] theorem Inf_insert {a : α} {s : set α} : Inf (insert a s) = a ⊓ Inf s :=
id ┴ └─┘ ┴ └─┘ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └─┘ └─┘ └────┘ ┴ ┴ └─┘
typ ┴ └─┘ ┴ └─┘ └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
doc └──┘ └─┘ └─┘
154 have Inf {b | b = a} = a,
id └─┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
155 from le_antisymm (Inf_le rfl) (le_Inf $ assume b b_eq, b_eq ▸ le_refl _),
id └─────────┘ └────┘ └─┘ └────┘ ┴ └──┘ └──┘ ┴ └─────┘
src └─────────┘ └────┘ └─┘ └────┘ ┴ └─────┘
typ └─────────┘ └────┘ └─┘ └────┘ ┴ └──┘ └──┘ ┴ └─────┘
156 calc Inf (insert a s) = Inf {b | b = a} ⊓ Inf s : Inf_union
id └─┘ └────┘ ┴ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ └───────┘
src └─┘ └────┘ └─┘ ┴ ┴ ┴ └─┘ └───────┘
typ └─┘ └────┘ ┴ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ └───────┘
doc └─┘ └─┘ └─┘
157 ... = a ⊓ Inf s : by rw [this]
id ┴ ┴ └─┘ ┴ └──┘
src ┴ └─┘ └──┘ └─
typ ┴ ┴ └─┘ ┴ └──┘└──┘└─
doc └─┘ └──┘ └─
txt └──┘ └─
par └──┘ └─
pid └┘ ┴└
st └───────┘┴└
158
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
159 @[simp] theorem Sup_singleton {a : α} : Sup {a} = a :=
id ┴ └─┘ ┴┴ ┴ ┴
src └─┘ ┴ ┴
typ ┴ └─┘ ┴┴ ┴ ┴
doc └──┘ └─┘
160 by finish [singleton_def]
id └───────────┘
src └──────┘└───────────┘└─
typ └──────┘└───────────┘└─
doc └──────┘ └─
txt └──────┘ └─
par └──────┘ └─
pid └┘ ┴└
st └───────────────────────
161 --eq.trans Sup_insert $ by simp
src ────────────────────────────────
typ ────────────────────────────────
doc ────────────────────────────────
txt ────────────────────────────────
par ────────────────────────────────
pid ────────────────────────────────
st ────────────────────────────────
162
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
163 @[simp] theorem Inf_singleton {a : α} : Inf {a} = a :=
id ┴ └─┘ ┴┴ ┴ ┴
src └─┘ ┴ ┴
typ ┴ └─┘ ┴┴ ┴ ┴
doc └──┘ └─┘
164 by finish [singleton_def]
id └───────────┘
src └──────┘└───────────┘└─
typ └──────┘└───────────┘└─
doc └──────┘ └─
txt └──────┘ └─
par └──────┘ └─
pid └┘ ┴└
st └───────────────────────
165 --eq.trans Inf_insert $ by simp
src ────────────────────────────────
typ ────────────────────────────────
doc ────────────────────────────────
txt ────────────────────────────────
par ────────────────────────────────
pid ────────────────────────────────
st ────────────────────────────────
166
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
167 @[simp] theorem Inf_eq_top : Inf s = ⊤ ↔ (∀a∈s, a = ⊤) :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─┘
168 iff.intro
id └───────┘
src └───────┘
typ └───────┘
169 (assume h a ha, top_unique $ h ▸ Inf_le ha)
id ┴ ┴ └┘ └────────┘ ┴ ┴ └────┘ └┘
src └────────┘ ┴ └────┘
typ ┴ ┴ └┘ └────────┘ ┴ ┴ └────┘ └┘
170 (assume h, top_unique $ le_Inf $ assume a ha, top_le_iff.2 $ h a ha)
id ┴ └────────┘ └────┘ ┴ └┘ └────────┘┴ ┴ ┴ └┘
src └────────┘ └────┘ └────────┘┴
typ ┴ └────────┘ └────┘ ┴ └┘ └────────┘┴ ┴ ┴ └┘
171
172 @[simp] theorem Sup_eq_bot : Sup s = ⊥ ↔ (∀a∈s, a = ⊥) :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─┘
173 iff.intro
id └───────┘
src └───────┘
typ └───────┘
174 (assume h a ha, bot_unique $ h ▸ le_Sup ha)
id ┴ ┴ └┘ └────────┘ ┴ ┴ └────┘ └┘
src └────────┘ ┴ └────┘
typ ┴ ┴ └┘ └────────┘ ┴ ┴ └────┘ └┘
175 (assume h, bot_unique $ Sup_le $ assume a ha, le_bot_iff.2 $ h a ha)
id ┴ └────────┘ └────┘ ┴ └┘ └────────┘┴ ┴ ┴ └┘
src └────────┘ └────┘ └────────┘┴
typ ┴ └────────┘ └────┘ ┴ └┘ └────────┘┴ ┴ ┴ └┘
176
177 end
178
179 section complete_linear_order
180 variables [complete_linear_order α] {s t : set α} {a b : α}
id └───────────────────┘ └─┘
src └───────────────────┘ └─┘
typ └───────────────────┘ └─┘
doc └───────────────────┘
181
182 lemma Inf_lt_iff : Inf s < b ↔ (∃a∈s, a < b) :=
id └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └─┘
183 iff.intro
id └───────┘
src └───────┘
typ └───────┘
184 (assume : Inf s < b, classical.by_contradiction $ assume : ¬ (∃a∈s, a < b),
id └─┘ ┴ ┴ ┴ └────────────────────────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src └─┘ ┴ └────────────────────────┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ └────────────────────────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └─┘
185 have b ≤ Inf s,
id ┴ ┴ └─┘ ┴
src ┴ └─┘
typ ┴ ┴ └─┘ ┴
doc └─┘
186 from le_Inf $ assume a ha, le_of_not_gt $ assume h, this ⟨a, ha, h⟩,
id └────┘ ┴ └┘ └──────────┘ ┴ └──┘ ┴ └┘ ┴
src └────┘ └──────────┘
typ └────┘ ┴ └┘ └──────────┘ ┴ └──┘ ┴ └┘ ┴
187 lt_irrefl b (lt_of_le_of_lt ‹b ≤ Inf s› ‹Inf s < b›))
id └───────┘ ┴ └────────────┘ ┴┴ ┴ └─┘ ┴┴ ┴└─┘ ┴ ┴ ┴┴
src └───────┘ └────────────┘ ┴ ┴ └─┘ ┴ ┴└─┘ ┴ ┴
typ └───────┘ ┴ └────────────┘ ┴┴ ┴ └─┘ ┴┴ ┴└─┘ ┴ ┴ ┴┴
doc ┴ └─┘ ┴ ┴└─┘ ┴
188 (assume ⟨a, ha, h⟩, lt_of_le_of_lt (Inf_le ha) h)
id ┴ └┘ ┴ └────────────┘ └────┘
src └────────────┘ └────┘
typ ┴ └┘ ┴ └────────────┘ └────┘
189
190 lemma lt_Sup_iff : b < Sup s ↔ (∃a∈s, b < a) :=
id ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └─┘
191 iff.intro
id └───────┘
src └───────┘
typ └───────┘
192 (assume : b < Sup s, classical.by_contradiction $ assume : ¬ (∃a∈s, b < a),
id ┴ ┴ └─┘ ┴ └────────────────────────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src ┴ └─┘ └────────────────────────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ └────────────────────────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └─┘
193 have Sup s ≤ b,
id └─┘ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴
doc └─┘
194 from Sup_le $ assume a ha, le_of_not_gt $ assume h, this ⟨a, ha, h⟩,
id └────┘ ┴ └┘ └──────────┘ ┴ └──┘ ┴ └┘ ┴
src └────┘ └──────────┘
typ └────┘ ┴ └┘ └──────────┘ ┴ └──┘ ┴ └┘ ┴
195 lt_irrefl b (lt_of_lt_of_le ‹b < Sup s› ‹Sup s ≤ b›))
id └───────┘ ┴ └────────────┘ ┴┴ ┴ └─┘ ┴┴ ┴└─┘ ┴ ┴ ┴┴
src └───────┘ └────────────┘ ┴ ┴ └─┘ ┴ ┴└─┘ ┴ ┴
typ └───────┘ ┴ └────────────┘ ┴┴ ┴ └─┘ ┴┴ ┴└─┘ ┴ ┴ ┴┴
doc ┴ └─┘ ┴ ┴└─┘ ┴
196 (assume ⟨a, ha, h⟩, lt_of_lt_of_le h $ le_Sup ha)
id ┴ └┘ ┴ └────────────┘ └────┘
src └────────────┘ └────┘
typ ┴ └┘ ┴ └────────────┘ └────┘
197
198 lemma Sup_eq_top : Sup s = ⊤ ↔ (∀b<⊤, ∃a∈s, b < a) :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └─┘
199 iff.intro
id └───────┘
src └───────┘
typ └───────┘
200 (assume (h : Sup s = ⊤) b hb, by rwa [←h, lt_Sup_iff] at hb)
id └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └────────┘
src └─┘ ┴ ┴ └────┘ └┘└────────┘└─────┘
typ └─┘ ┴ ┴ ┴ ┴ └┘ └────┘┴└┘└────────┘└─────┘
doc └─┘ └────┘ └┘ └─────┘
txt └────┘ └┘ └─────┘
par └────┘ └┘ └─────┘
pid └─┘ └┘ ┴└────┘
st └──────┘└──────────┘┴└────┘
201 (assume h, top_unique $ le_of_not_gt $ assume h',
id ┴ └────────┘ └──────────┘ └┘
src └────────┘ └──────────┘
typ ┴ └────────┘ └──────────┘ └┘
202 let ⟨a, ha, h⟩ := h _ h' in
id └─┘ ┴ └┘ ┴ ┴ └┘
typ └─┘ ┴ └┘ ┴ ┴ └┘
203 lt_irrefl a $ lt_of_le_of_lt (le_Sup ha) h)
id └───────┘ └────────────┘ └────┘
src └───────┘ └────────────┘ └────┘
typ └───────┘ └────────────┘ └────┘
204
205 lemma Inf_eq_bot : Inf s = ⊥ ↔ (∀b>⊥, ∃a∈s, a < b) :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └─┘
206 iff.intro
id └───────┘
src └───────┘
typ └───────┘
207 (assume (h : Inf s = ⊥) b (hb : ⊥ < b), by rwa [←h, Inf_lt_iff] at hb)
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘
src └─┘ ┴ ┴ ┴ ┴ └────┘ └┘└────────┘└─────┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘┴└┘└────────┘└─────┘
doc └─┘ └────┘ └┘ └─────┘
txt └────┘ └┘ └─────┘
par └────┘ └┘ └─────┘
pid └─┘ └┘ ┴└────┘
st └──────┘└──────────┘┴└────┘
208 (assume h, bot_unique $ le_of_not_gt $ assume h',
id ┴ └────────┘ └──────────┘ └┘
src └────────┘ └──────────┘
typ ┴ └────────┘ └──────────┘ └┘
209 let ⟨a, ha, h⟩ := h _ h' in
id └─┘ ┴ └┘ ┴ ┴ └┘
typ └─┘ ┴ └┘ ┴ ┴ └┘
210 lt_irrefl a $ lt_of_lt_of_le h (Inf_le ha))
id └───────┘ └────────────┘ └────┘
src └───────┘ └────────────┘ └────┘
typ └───────┘ └────────────┘ └────┘
211
212 lemma lt_supr_iff {ι : Sort*} {f : ι → α} : a < supr f ↔ (∃i, a < f i) :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
doc └──┘
213 iff.trans lt_Sup_iff $ iff.intro
id └───────┘ └────────┘ └───────┘
src └───────┘ └────────┘ └───────┘
typ └───────┘ └────────┘ └───────┘
214 (assume ⟨a', ⟨i, rfl⟩, ha⟩, ⟨i, ha⟩)
id ┴ ┴ └─┘ └┘
src └─┘
typ ┴ ┴ └─┘ └┘
215 (assume ⟨i, hi⟩, ⟨f i, ⟨i, rfl⟩, hi⟩)
id ┴┴ └┘ ┴ └─┘
src └─┘
typ ┴┴ └┘ ┴ └─┘
216
217 lemma infi_lt_iff {ι : Sort*} {f : ι → α} : infi f < a ↔ (∃i, f i < a) :=
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
doc └──┘
218 iff.trans Inf_lt_iff $ iff.intro
id └───────┘ └────────┘ └───────┘
src └───────┘ └────────┘ └───────┘
typ └───────┘ └────────┘ └───────┘
219 (assume ⟨a', ⟨i, rfl⟩, ha⟩, ⟨i, ha⟩)
id ┴ ┴ └─┘ └┘
src └─┘
typ ┴ ┴ └─┘ └┘
220 (assume ⟨i, hi⟩, ⟨f i, ⟨i, rfl⟩, hi⟩)
id ┴┴ └┘ ┴ └─┘
src └─┘
typ ┴┴ └┘ ┴ └─┘
221
222 end complete_linear_order
223
224 /- supr & infi -/
225
226 section
227 variables [complete_lattice α] {s t : ι → α} {a b : α}
id └──────────────┘
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
228
229 -- TODO: this declaration gives error when starting smt state
230 --@[ematch]
231 theorem le_supr (s : ι → α) (i : ι) : s i ≤ supr s :=
id ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
src ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
doc └──┘
232 le_Sup ⟨i, rfl⟩
id └────┘ ┴ └─┘
src └────┘ └─┘
typ └────┘ ┴ └─┘
233
234 @[ematch] theorem le_supr' (s : ι → α) (i : ι) : (: s i ≤ supr s :) :=
id ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
src └────┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
doc └────┘ └──┘
235 le_Sup ⟨i, rfl⟩
id └────┘ ┴ └─┘
src └────┘ └─┘
typ └────┘ ┴ └─┘
236
237 /- TODO: this version would be more powerful, but, alas, the pattern matcher
238 doesn't accept it.
239 @[ematch] theorem le_supr' (s : ι → α) (i : ι) : (: s i :) ≤ (: supr s :) :=
240 le_Sup ⟨i, rfl⟩
241 -/
242
243 lemma is_lub_supr : is_lub (range s) (⨆j, s j) := is_lub_Sup
id └────┘ └───┘ ┴ ┴┴┴ ┴ ┴ └────────┘
src └────┘ └───┘ ┴ ┴ └────────┘
typ └────┘ └───┘ ┴ ┴┴┴ ┴ ┴ └────────┘
doc └────┘ └───┘ ┴ ┴
244
245 lemma is_lub_iff_supr_eq : is_lub (range s) a ↔ (⨆j, s j) = a := is_lub_iff_eq_of_is_lub is_lub_supr
id └────┘ └───┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └─────────────────────┘ └─────────┘
src └────┘ └───┘ ┴ ┴ ┴ ┴ └─────────────────────┘ └─────────┘
typ └────┘ └───┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └─────────────────────┘ └─────────┘
doc └────┘ └───┘ ┴ ┴
246
247 lemma is_glb_infi : is_glb (range s) (⨅j, s j) := is_glb_Inf
id └────┘ └───┘ ┴ ┴┴┴ ┴ ┴ └────────┘
src └────┘ └───┘ ┴ ┴ └────────┘
typ └────┘ └───┘ ┴ ┴┴┴ ┴ ┴ └────────┘
doc └────┘ └───┘ ┴ ┴
248
249 lemma is_glb_iff_infi_eq : is_glb (range s) a ↔ (⨅j, s j) = a := is_glb_iff_eq_of_is_glb is_glb_infi
id └────┘ └───┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └─────────────────────┘ └─────────┘
src └────┘ └───┘ ┴ ┴ ┴ ┴ └─────────────────────┘ └─────────┘
typ └────┘ └───┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └─────────────────────┘ └─────────┘
doc └────┘ └───┘ ┴ ┴
250
251 theorem le_supr_of_le (i : ι) (h : a ≤ s i) : a ≤ supr s :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
src ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
doc └──┘
252 le_trans h (le_supr _ i)
id └──────┘ ┴ └─────┘ ┴
src └──────┘ └─────┘
typ └──────┘ ┴ └─────┘ ┴
253
254 theorem supr_le (h : ∀i, s i ≤ a) : supr s ≤ a :=
id ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘
255 Sup_le $ assume b ⟨i, eq⟩, eq ▸ h i
id └────┘ ┴ ┴┴ └┘ ┴ ┴
src └────┘ └┘ ┴
typ └────┘ ┴ ┴┴ └┘ ┴ ┴
256
257 theorem supr_le_supr (h : ∀i, s i ≤ t i) : supr s ≤ supr t :=
id ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src ┴ └──┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──┘ └──┘
258 supr_le $ assume i, le_supr_of_le i (h i)
id └─────┘ ┴ └───────────┘ ┴ ┴ ┴
src └─────┘ └───────────┘
typ └─────┘ ┴ └───────────┘ ┴ ┴ ┴
259
260 theorem supr_le_supr2 {t : ι₂ → α} (h : ∀i, ∃j, s i ≤ t j) : supr s ≤ supr t :=
id └┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src ┴ ┴ ┴ └──┘ ┴ └──┘
typ └┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──┘ └──┘
261 supr_le $ assume j, exists.elim (h j) le_supr_of_le
id └─────┘ ┴ └─────────┘ ┴ ┴ └───────────┘
src └─────┘ └─────────┘ └───────────┘
typ └─────┘ ┴ └─────────┘ ┴ ┴ └───────────┘
262
263 theorem supr_le_supr_const (h : ι → ι₂) : (⨆ i:ι, a) ≤ (⨆ j:ι₂, a) :=
id ┴ └┘ ┴ ┴┴ ┴ ┴ ┴ └┘┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴┴ ┴ ┴ ┴ └┘┴ ┴
doc ┴ ┴ ┴ ┴
264 supr_le $ le_supr _ ∘ h
id └─────┘ └─────┘ ┴ ┴
src └─────┘ └─────┘ ┴
typ └─────┘ └─────┘ ┴ ┴
265
266 @[simp] theorem supr_le_iff : supr s ≤ a ↔ (∀i, s i ≤ a) :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘
267 ⟨assume : supr s ≤ a, assume i, le_trans (le_supr _ _) this, supr_le⟩
id └──┘ ┴ ┴ ┴ ┴ └──────┘ └─────┘ └──┘ └─────┘
src └──┘ ┴ └──────┘ └─────┘ └─────┘
typ └──┘ ┴ ┴ ┴ ┴ └──────┘ └─────┘ └──┘ └─────┘
doc └──┘
268
269 -- TODO: finish doesn't do well here.
270 @[congr] theorem supr_congr_Prop {α : Type u} [has_Sup α] {p q : Prop} {f₁ : p → α} {f₂ : q → α}
id └─────┘ ┴ ┴ ┴ ┴ ┴
src └───┘ └─────┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴
doc └───┘ └─────┘
271 (pq : p ↔ q) (f : ∀x, f₁ (pq.mpr x) = f₂ x) : supr f₁ = supr f₂ :=
id ┴ ┴ ┴ ┴ └┘ └┘└──┘ ┴ ┴ └┘ ┴ └──┘ └┘ ┴ └──┘ └┘
src ┴ └──┘ ┴ └──┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ └┘ └┘└──┘ ┴ ┴ └┘ ┴ └──┘ └┘ ┴ └──┘ └┘
doc └──┘ └──┘
272 begin
st └─────
273 unfold supr,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
274 apply congr_arg,
id └───────┘
src └────┘└───────┘
typ └────┘└───────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────┘└─
275 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
276 simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────┘└─
277 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
278 exact λ⟨h, W⟩, ⟨pq.1 h, eq.trans (f (pq.1 h)).symm W⟩,
id ┴ ┴ └──────┘ ┴ └┘
src └────┘ ┴ └┘ └─┘ └─┘ └┘└──────┘┴ ┴ └─┘ └──────┘ ┴
typ └────┘ ┴┴└┘┴└─┘ └─┘ └┘└──────┘┴ ┴┴ └┘└─┘ └──────┘ ┴
doc └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └─┘ └──────┘ ┴
txt └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └─┘ └──────┘ ┴
par └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └─┘ └──────┘ ┴
pid ┴ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └─┘ └──────┘ ┴
st ──────────────────────────────────────────────────────┘└─
279 exact λ⟨h, W⟩, ⟨pq.2 h, eq.trans (f h) W⟩
id ┴ ┴ └┘ └──────┘ ┴
src └────┘ ┴ └┘ └─┘ └─┘ └┘└──────┘┴ ┴ └┘ └┘
typ └────┘ ┴┴└┘┴└─┘ └┘└─┘ └┘└──────┘┴ ┴┴ └┘ └┘
doc └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └┘ └┘
txt └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └┘ └┘
par └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └┘ └┘
pid ┴ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └┘ ┴┴
st ───────────────────────────────────────────┘
280 end
st └─┘
281
282 theorem infi_le (s : ι → α) (i : ι) : infi s ≤ s i :=
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └──┘ ┴
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘
283 Inf_le ⟨i, rfl⟩
id └────┘ ┴ └─┘
src └────┘ └─┘
typ └────┘ ┴ └─┘
284
285 @[ematch] theorem infi_le' (s : ι → α) (i : ι) : (: infi s ≤ s i :) :=
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └────┘ └──┘ ┴
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └────┘ └──┘
286 Inf_le ⟨i, rfl⟩
id └────┘ ┴ └─┘
src └────┘ └─┘
typ └────┘ ┴ └─┘
287
288 /- I wanted to see if this would help for infi_comm; it doesn't.
289 @[ematch] theorem infi_le₂' (s : ι → ι₂ → α) (i : ι) (j : ι₂) : (: ⨅ i j, s i j :) ≤ (: s i j :) :=
290 begin
291 transitivity,
292 apply (infi_le (λ i, ⨅ j, s i j) i),
293 apply infi_le
294 end
295 -/
296
297 theorem infi_le_of_le (i : ι) (h : s i ≤ a) : infi s ≤ a :=
id ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘
298 le_trans (infi_le _ i) h
id └──────┘ └─────┘ ┴ ┴
src └──────┘ └─────┘
typ └──────┘ └─────┘ ┴ ┴
299
300 theorem le_infi (h : ∀i, a ≤ s i) : a ≤ infi s :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
src ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
doc └──┘
301 le_Inf $ assume b ⟨i, eq⟩, eq ▸ h i
id └────┘ ┴ ┴┴ └┘ ┴ ┴
src └────┘ └┘ ┴
typ └────┘ ┴ ┴┴ └┘ ┴ ┴
302
303 theorem infi_le_infi (h : ∀i, s i ≤ t i) : infi s ≤ infi t :=
id ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src ┴ └──┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──┘ └──┘
304 le_infi $ assume i, infi_le_of_le i (h i)
id └─────┘ ┴ └───────────┘ ┴ ┴ ┴
src └─────┘ └───────────┘
typ └─────┘ ┴ └───────────┘ ┴ ┴ ┴
305
306 theorem infi_le_infi2 {t : ι₂ → α} (h : ∀j, ∃i, s i ≤ t j) : infi s ≤ infi t :=
id └┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src ┴ ┴ ┴ └──┘ ┴ └──┘
typ └┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──┘ └──┘
307 le_infi $ assume j, exists.elim (h j) infi_le_of_le
id └─────┘ ┴ └─────────┘ ┴ ┴ └───────────┘
src └─────┘ └─────────┘ └───────────┘
typ └─────┘ ┴ └─────────┘ ┴ ┴ └───────────┘
308
309 theorem infi_le_infi_const (h : ι₂ → ι) : (⨅ i:ι, a) ≤ (⨅ j:ι₂, a) :=
id └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └┘┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └┘┴ ┴
doc ┴ ┴ ┴ ┴
310 le_infi $ infi_le _ ∘ h
id └─────┘ └─────┘ ┴ ┴
src └─────┘ └─────┘ ┴
typ └─────┘ └─────┘ ┴ ┴
311
312 @[simp] theorem le_infi_iff : a ≤ infi s ↔ (∀i, a ≤ s i) :=
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘
313 ⟨assume : a ≤ infi s, assume i, le_trans this (infi_le _ _), le_infi⟩
id ┴ ┴ └──┘ ┴ ┴ └──────┘ └──┘ └─────┘ └─────┘
src ┴ └──┘ └──────┘ └─────┘ └─────┘
typ ┴ ┴ └──┘ ┴ ┴ └──────┘ └──┘ └─────┘ └─────┘
doc └──┘
314
315 @[congr] theorem infi_congr_Prop {α : Type u} [has_Inf α] {p q : Prop} {f₁ : p → α} {f₂ : q → α}
id └─────┘ ┴ ┴ ┴ ┴ ┴
src └───┘ └─────┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴
doc └───┘ └─────┘
316 (pq : p ↔ q) (f : ∀x, f₁ (pq.mpr x) = f₂ x) : infi f₁ = infi f₂ :=
id ┴ ┴ ┴ ┴ └┘ └┘└──┘ ┴ ┴ └┘ ┴ └──┘ └┘ ┴ └──┘ └┘
src ┴ └──┘ ┴ └──┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ └┘ └┘└──┘ ┴ ┴ └┘ ┴ └──┘ └┘ ┴ └──┘ └┘
doc └──┘ └──┘
317 begin
st └─────
318 unfold infi,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
319 apply congr_arg,
id └───────┘
src └────┘└───────┘
typ └────┘└───────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────┘└─
320 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
321 simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────┘└─
322 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
323 exact λ⟨h, W⟩, ⟨pq.1 h, eq.trans (f (pq.1 h)).symm W⟩,
id ┴ ┴ └──────┘ ┴ └┘
src └────┘ ┴ └┘ └─┘ └─┘ └┘└──────┘┴ ┴ └─┘ └──────┘ ┴
typ └────┘ ┴┴└┘┴└─┘ └─┘ └┘└──────┘┴ ┴┴ └┘└─┘ └──────┘ ┴
doc └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └─┘ └──────┘ ┴
txt └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └─┘ └──────┘ ┴
par └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └─┘ └──────┘ ┴
pid ┴ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └─┘ └──────┘ ┴
st ──────────────────────────────────────────────────────┘└─
324 exact λ⟨h, W⟩, ⟨pq.2 h, eq.trans (f h) W⟩
id ┴ ┴ └┘ └──────┘ ┴
src └────┘ ┴ └┘ └─┘ └─┘ └┘└──────┘┴ ┴ └┘ └┘
typ └────┘ ┴┴└┘┴└─┘ └┘└─┘ └┘└──────┘┴ ┴┴ └┘ └┘
doc └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └┘ └┘
txt └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └┘ └┘
par └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └┘ └┘
pid ┴ ┴ └┘ └─┘ └─┘ └┘ ┴ ┴ └┘ ┴┴
st ───────────────────────────────────────────┘
325 end
st └─┘
326
327 @[simp] theorem infi_const {a : α} : ∀[nonempty ι], (⨅ b:ι, a) = a
id ┴ ┴└──────┘ ┴ ┴ ┴┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴
typ ┴ ┴└──────┘ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
328 | ⟨i⟩ := le_antisymm (Inf_le ⟨i, rfl⟩) (by finish)
id ┴ └─────────┘ └────┘ └─┘
src └─────────┘ └────┘ └─┘ └────┘
typ ┴ └─────────┘ └────┘ └─┘ └────┘
doc └────┘
txt └────┘
par └────┘
st └─────┘
329
330 @[simp] theorem supr_const {a : α} : ∀[nonempty ι], (⨆ b:ι, a) = a
id ┴ ┴└──────┘ ┴ ┴ ┴┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴
typ ┴ ┴└──────┘ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
331 | ⟨i⟩ := le_antisymm (by finish) (le_Sup ⟨i, rfl⟩)
id ┴ └─────────┘ └────┘ └─┘
src └─────────┘ └────┘ └────┘ └─┘
typ ┴ └─────────┘ └────┘ └────┘ └─┘
doc └────┘
txt └────┘
par └────┘
st └─────┘
332
333 @[simp] lemma infi_top : (⨅i:ι, ⊤ : α) = ⊤ :=
id ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
334 top_unique $ le_infi $ assume i, le_refl _
id └────────┘ └─────┘ ┴ └─────┘
src └────────┘ └─────┘ └─────┘
typ └────────┘ └─────┘ ┴ └─────┘
335
336 @[simp] lemma supr_bot : (⨆i:ι, ⊥ : α) = ⊥ :=
id ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
337 bot_unique $ supr_le $ assume i, le_refl _
id └────────┘ └─────┘ ┴ └─────┘
src └────────┘ └─────┘ └─────┘
typ └────────┘ └─────┘ ┴ └─────┘
338
339 @[simp] lemma infi_eq_top : infi s = ⊤ ↔ (∀i, s i = ⊤) :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘
340 iff.intro
id └───────┘
src └───────┘
typ └───────┘
341 (assume eq i, top_unique $ eq ▸ infi_le _ _)
id └┘ ┴ └────────┘ └┘ ┴ └─────┘
src └┘ └────────┘ └┘ ┴ └─────┘
typ └┘ ┴ └────────┘ └┘ ┴ └─────┘
342 (assume h, top_unique $ le_infi $ assume i, top_le_iff.2 $ h i)
id ┴ └────────┘ └─────┘ ┴ └────────┘┴ ┴ ┴
src └────────┘ └─────┘ └────────┘┴
typ ┴ └────────┘ └─────┘ ┴ └────────┘┴ ┴ ┴
343
344 @[simp] lemma supr_eq_bot : supr s = ⊥ ↔ (∀i, s i = ⊥) :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘
345 iff.intro
id └───────┘
src └───────┘
typ └───────┘
346 (assume eq i, bot_unique $ eq ▸ le_supr _ _)
id └┘ ┴ └────────┘ └┘ ┴ └─────┘
src └┘ └────────┘ └┘ ┴ └─────┘
typ └┘ ┴ └────────┘ └┘ ┴ └─────┘
347 (assume h, bot_unique $ supr_le $ assume i, le_bot_iff.2 $ h i)
id ┴ └────────┘ └─────┘ ┴ └────────┘┴ ┴ ┴
src └────────┘ └─────┘ └────────┘┴
typ ┴ └────────┘ └─────┘ ┴ └────────┘┴ ┴ ┴
348
349 @[simp] lemma infi_pos {p : Prop} {f : p → α} (hp : p) : (⨅ h : p, f h) = f hp :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘
doc └──┘ ┴ ┴
350 le_antisymm (infi_le _ _) (le_infi $ assume h, le_refl _)
id └─────────┘ └─────┘ └─────┘ ┴ └─────┘
src └─────────┘ └─────┘ └─────┘ └─────┘
typ └─────────┘ └─────┘ └─────┘ ┴ └─────┘
351
352 @[simp] lemma infi_neg {p : Prop} {f : p → α} (hp : ¬ p) : (⨅ h : p, f h) = ⊤ :=
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
353 le_antisymm le_top $ le_infi $ assume h, (hp h).elim
id └─────────┘ └────┘ └─────┘ ┴ └┘ ┴ └──┘
src └─────────┘ └────┘ └─────┘ └──┘
typ └─────────┘ └────┘ └─────┘ ┴ └┘ ┴ └──┘
354
355 @[simp] lemma supr_pos {p : Prop} {f : p → α} (hp : p) : (⨆ h : p, f h) = f hp :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘
doc └──┘ ┴ ┴
356 le_antisymm (supr_le $ assume h, le_refl _) (le_supr _ _)
id └─────────┘ └─────┘ ┴ └─────┘ └─────┘
src └─────────┘ └─────┘ └─────┘ └─────┘
typ └─────────┘ └─────┘ ┴ └─────┘ └─────┘
357
358 @[simp] lemma supr_neg {p : Prop} {f : p → α} (hp : ¬ p) : (⨆ h : p, f h) = ⊥ :=
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
359 le_antisymm (supr_le $ assume h, (hp h).elim) bot_le
id └─────────┘ └─────┘ ┴ └┘ ┴ └──┘ └────┘
src └─────────┘ └─────┘ └──┘ └────┘
typ └─────────┘ └─────┘ ┴ └┘ ┴ └──┘ └────┘
360
361 lemma supr_eq_dif {p : Prop} [decidable p] (a : p → α) :
id └───────┘ ┴ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴ ┴
362 (⨆h:p, a h) = (if h : p then a h else ⊥) :=
id ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └┘ ┴
typ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc ┴ ┴
363 by by_cases p; simp [h]
id ┴ ┴
src └───────┘ └────┘ └─
typ └───────┘┴ └────┘┴└─
doc └───────┘ └────┘ └─
txt └───────┘ └────┘ └─
par └───────┘ └────┘ └─
pid ┴ ┴┴ ┴└
st └─────────────────────
364
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
365 lemma supr_eq_if {p : Prop} [decidable p] (a : α) :
id └───────┘ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴
366 (⨆h:p, a) = (if p then a else ⊥) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
367 by rw [supr_eq_dif, dif_eq_if]
id └─────────┘ └───────┘
src └──┘└─────────┘└┘└───────┘└─
typ └──┘└─────────┘└┘└───────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └──────────────┘└─────────┘┴└
368
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
369 lemma infi_eq_dif {p : Prop} [decidable p] (a : p → α) :
id └───────┘ ┴ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴ ┴
370 (⨅h:p, a h) = (if h : p then a h else ⊤) :=
id ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └┘ ┴
typ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc ┴ ┴
371 by by_cases p; simp [h]
id ┴ ┴
src └───────┘ └────┘ └─
typ └───────┘┴ └────┘┴└─
doc └───────┘ └────┘ └─
txt └───────┘ └────┘ └─
par └───────┘ └────┘ └─
pid ┴ ┴┴ ┴└
st └─────────────────────
372
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
373 lemma infi_eq_if {p : Prop} [decidable p] (a : α) :
id └───────┘ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴
374 (⨅h:p, a) = (if p then a else ⊤) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
375 by rw [infi_eq_dif, dif_eq_if]
id └─────────┘ └───────┘
src └──┘└─────────┘└┘└───────┘└─
typ └──┘└─────────┘└┘└───────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └──────────────┘└─────────┘┴└
376
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
377 -- TODO: should this be @[simp]?
src ────────────────────────────────┘
typ ────────────────────────────────┘
doc ────────────────────────────────┘
txt ────────────────────────────────┘
par ────────────────────────────────┘
pid ────────────────────────────────┘
st ────────────────────────────────┘
378 theorem infi_comm {f : ι → ι₂ → α} : (⨅i, ⨅j, f i j) = (⨅j, ⨅i, f i j) :=
id ┴ └┘ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
379 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
380 (le_infi $ assume i, le_infi $ assume j, infi_le_of_le j $ infi_le _ i)
id └─────┘ ┴ └─────┘ ┴ └───────────┘ ┴ └─────┘ ┴
src └─────┘ └─────┘ └───────────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ └───────────┘ ┴ └─────┘ ┴
381 (le_infi $ assume j, le_infi $ assume i, infi_le_of_le i $ infi_le _ j)
id └─────┘ ┴ └─────┘ ┴ └───────────┘ ┴ └─────┘ ┴
src └─────┘ └─────┘ └───────────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ └───────────┘ ┴ └─────┘ ┴
382
383 /- TODO: this is strange. In the proof below, we get exactly the desired
384 among the equalities, but close does not get it.
385 begin
386 apply @le_antisymm,
387 simp, intros,
388 begin [smt]
389 ematch, ematch, ematch, trace_state, have := le_refl (f i_1 i),
390 trace_state, close
391 end
392 end
393 -/
394
395 -- TODO: should this be @[simp]?
396 theorem supr_comm {f : ι → ι₂ → α} : (⨆i, ⨆j, f i j) = (⨆j, ⨆i, f i j) :=
id ┴ └┘ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
397 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
398 (supr_le $ assume i, supr_le $ assume j, le_supr_of_le j $ le_supr _ i)
id └─────┘ ┴ └─────┘ ┴ └───────────┘ ┴ └─────┘ ┴
src └─────┘ └─────┘ └───────────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ └───────────┘ ┴ └─────┘ ┴
399 (supr_le $ assume j, supr_le $ assume i, le_supr_of_le i $ le_supr _ j)
id └─────┘ ┴ └─────┘ ┴ └───────────┘ ┴ └─────┘ ┴
src └─────┘ └─────┘ └───────────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ └───────────┘ ┴ └─────┘ ┴
400
401 @[simp] theorem infi_infi_eq_left {b : β} {f : Πx:β, x = b → α} : (⨅x, ⨅h:x = b, f x h) = f b rfl :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ ┴ ┴ ┴ ┴
402 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
403 (infi_le_of_le b $ infi_le _ rfl)
id └───────────┘ ┴ └─────┘ └─┘
src └───────────┘ └─────┘ └─┘
typ └───────────┘ ┴ └─────┘ └─┘
404 (le_infi $ assume b', le_infi $ assume eq, match b', eq with ._, rfl := le_refl _ end)
id └─────┘ └┘ └─────┘ └┘ └┘ └┘ └─┘ └─────┘
src └─────┘ └─────┘ └┘ └┘ └─┘ └─────┘
typ └─────┘ └┘ └─────┘ └┘ └┘ └┘ └─┘ └─────┘
405
406 @[simp] theorem infi_infi_eq_right {b : β} {f : Πx:β, b = x → α} : (⨅x, ⨅h:b = x, f x h) = f b rfl :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ ┴ ┴ ┴ ┴
407 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
408 (infi_le_of_le b $ infi_le _ rfl)
id └───────────┘ ┴ └─────┘ └─┘
src └───────────┘ └─────┘ └─┘
typ └───────────┘ ┴ └─────┘ └─┘
409 (le_infi $ assume b', le_infi $ assume eq, match b', eq with ._, rfl := le_refl _ end)
id └─────┘ └┘ └─────┘ └┘ └┘ └┘ └─┘ └─────┘
src └─────┘ └─────┘ └┘ └┘ └─┘ └─────┘
typ └─────┘ └┘ └─────┘ └┘ └┘ └┘ └─┘ └─────┘
410
411 @[simp] theorem supr_supr_eq_left {b : β} {f : Πx:β, x = b → α} : (⨆x, ⨆h : x = b, f x h) = f b rfl :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ ┴ ┴ ┴ ┴
412 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
413 (supr_le $ assume b', supr_le $ assume eq, match b', eq with ._, rfl := le_refl _ end)
id └─────┘ └┘ └─────┘ └┘ └┘ └┘ └─┘ └─────┘
src └─────┘ └─────┘ └┘ └┘ └─┘ └─────┘
typ └─────┘ └┘ └─────┘ └┘ └┘ └┘ └─┘ └─────┘
414 (le_supr_of_le b $ le_supr _ rfl)
id └───────────┘ ┴ └─────┘ └─┘
src └───────────┘ └─────┘ └─┘
typ └───────────┘ ┴ └─────┘ └─┘
415
416 @[simp] theorem supr_supr_eq_right {b : β} {f : Πx:β, b = x → α} : (⨆x, ⨆h : b = x, f x h) = f b rfl :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ ┴ ┴ ┴ ┴
417 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
418 (supr_le $ assume b', supr_le $ assume eq, match b', eq with ._, rfl := le_refl _ end)
id └─────┘ └┘ └─────┘ └┘ └┘ └┘ └─┘ └─────┘
src └─────┘ └─────┘ └┘ └┘ └─┘ └─────┘
typ └─────┘ └┘ └─────┘ └┘ └┘ └┘ └─┘ └─────┘
419 (le_supr_of_le b $ le_supr _ rfl)
id └───────────┘ ┴ └─────┘ └─┘
src └───────────┘ └─────┘ └─┘
typ └───────────┘ ┴ └─────┘ └─┘
420
421 attribute [ematch] le_refl
id └─────┘
src └────┘ └─────┘
typ └─────┘
doc └────┘
422
423 theorem infi_inf_eq {f g : ι → α} : (⨅ x, f x ⊓ g x) = (⨅ x, f x) ⊓ (⨅ x, g x) :=
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
424 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
425 (le_inf
id └────┘
src └────┘
typ └────┘
426 (le_infi $ assume i, infi_le_of_le i inf_le_left)
id └─────┘ ┴ └───────────┘ ┴ └─────────┘
src └─────┘ └───────────┘ └─────────┘
typ └─────┘ ┴ └───────────┘ ┴ └─────────┘
427 (le_infi $ assume i, infi_le_of_le i inf_le_right))
id └─────┘ ┴ └───────────┘ ┴ └──────────┘
src └─────┘ └───────────┘ └──────────┘
typ └─────┘ ┴ └───────────┘ ┴ └──────────┘
428 (le_infi $ assume i, le_inf
id └─────┘ ┴ └────┘
src └─────┘ └────┘
typ └─────┘ ┴ └────┘
429 (inf_le_left_of_le $ infi_le _ _)
id └───────────────┘ └─────┘
src └───────────────┘ └─────┘
typ └───────────────┘ └─────┘
430 (inf_le_right_of_le $ infi_le _ _))
id └────────────────┘ └─────┘
src └────────────────┘ └─────┘
typ └────────────────┘ └─────┘
431
432 /- TODO: here is another example where more flexible pattern matching
433 might help.
434
435 begin
436 apply @le_antisymm,
437 safe, pose h := f a ⊓ g a, begin [smt] ematch, ematch end
438 end
439 -/
440
441 lemma infi_inf {f : ι → α} {a : α} (i : ι) : (⨅x, f x) ⊓ a = (⨅ x, f x ⊓ a) :=
id ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
442 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
443 (le_infi $ assume i, le_inf (inf_le_left_of_le $ infi_le _ _) inf_le_right)
id └─────┘ ┴ └────┘ └───────────────┘ └─────┘ └──────────┘
src └─────┘ └────┘ └───────────────┘ └─────┘ └──────────┘
typ └─────┘ ┴ └────┘ └───────────────┘ └─────┘ └──────────┘
444 (le_inf (infi_le_infi $ assume i, inf_le_left) (infi_le_of_le i inf_le_right))
id └────┘ └──────────┘ ┴ └─────────┘ └───────────┘ ┴ └──────────┘
src └────┘ └──────────┘ └─────────┘ └───────────┘ └──────────┘
typ └────┘ └──────────┘ ┴ └─────────┘ └───────────┘ ┴ └──────────┘
445
446 lemma inf_infi {f : ι → α} {a : α} (i : ι) : a ⊓ (⨅x, f x) = (⨅ x, a ⊓ f x) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
447 by rw [inf_comm, infi_inf i]; simp [inf_comm]
id └──────┘ └──────┘ ┴ └──────┘
src └──┘└──────┘└┘└──────┘┴ ┴ └────┘└──────┘└─
typ └──┘└──────┘└┘└──────┘┴┴┴ └────┘└──────┘└─
doc └──┘ └┘ ┴ ┴ └────┘ └─
txt └──┘ └┘ ┴ ┴ └────┘ └─
par └──┘ └┘ ┴ ┴ └────┘ └─
pid └┘ └┘ ┴ ┴ ┴┴ ┴└
st └───────────┘└──────────┘┴└─────────────────
448
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
449 lemma binfi_inf {ι : Sort*} {p : ι → Prop}
id ┴
typ ┴
450 {f : Πi, p i → α} {a : α} {i : ι} (hi : p i) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
451 (⨅i (h : p i), f i h) ⊓ a = (⨅ i (h : p i), f i h ⊓ a) :=
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
452 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
453 (le_infi $ assume i, le_infi $ assume hi,
id └─────┘ ┴ └─────┘ └┘
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ └┘
454 le_inf (inf_le_left_of_le $ infi_le_of_le i $ infi_le _ _) inf_le_right)
id └────┘ └───────────────┘ └───────────┘ ┴ └─────┘ └──────────┘
src └────┘ └───────────────┘ └───────────┘ └─────┘ └──────────┘
typ └────┘ └───────────────┘ └───────────┘ ┴ └─────┘ └──────────┘
455 (le_inf (infi_le_infi $ assume i, infi_le_infi $ assume hi, inf_le_left)
id └────┘ └──────────┘ ┴ └──────────┘ └┘ └─────────┘
src └────┘ └──────────┘ └──────────┘ └─────────┘
typ └────┘ └──────────┘ ┴ └──────────┘ └┘ └─────────┘
456 (infi_le_of_le i $ infi_le_of_le hi $ inf_le_right))
id └───────────┘ ┴ └───────────┘ └┘ └──────────┘
src └───────────┘ └───────────┘ └──────────┘
typ └───────────┘ ┴ └───────────┘ └┘ └──────────┘
457
458 theorem supr_sup_eq {f g : β → α} : (⨆ x, f x ⊔ g x) = (⨆ x, f x) ⊔ (⨆ x, g x) :=
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
459 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
460 (supr_le $ assume i, sup_le
id └─────┘ ┴ └────┘
src └─────┘ └────┘
typ └─────┘ ┴ └────┘
461 (le_sup_left_of_le $ le_supr _ _)
id └───────────────┘ └─────┘
src └───────────────┘ └─────┘
typ └───────────────┘ └─────┘
462 (le_sup_right_of_le $ le_supr _ _))
id └────────────────┘ └─────┘
src └────────────────┘ └─────┘
typ └────────────────┘ └─────┘
463 (sup_le
id └────┘
src └────┘
typ └────┘
464 (supr_le $ assume i, le_supr_of_le i le_sup_left)
id └─────┘ ┴ └───────────┘ ┴ └─────────┘
src └─────┘ └───────────┘ └─────────┘
typ └─────┘ ┴ └───────────┘ ┴ └─────────┘
465 (supr_le $ assume i, le_supr_of_le i le_sup_right))
id └─────┘ ┴ └───────────┘ ┴ └──────────┘
src └─────┘ └───────────┘ └──────────┘
typ └─────┘ ┴ └───────────┘ ┴ └──────────┘
466
467 /- supr and infi under Prop -/
468
469 @[simp] theorem infi_false {s : false → α} : infi s = ⊤ :=
id └───┘ ┴ └──┘ ┴ ┴ ┴
src └───┘ └──┘ ┴ ┴
typ └───┘ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
470 le_antisymm le_top (le_infi $ assume i, false.elim i)
id └─────────┘ └────┘ └─────┘ ┴ └────────┘ ┴
src └─────────┘ └────┘ └─────┘ └────────┘
typ └─────────┘ └────┘ └─────┘ ┴ └────────┘ ┴
471
472 @[simp] theorem supr_false {s : false → α} : supr s = ⊥ :=
id └───┘ ┴ └──┘ ┴ ┴ ┴
src └───┘ └──┘ ┴ ┴
typ └───┘ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
473 le_antisymm (supr_le $ assume i, false.elim i) bot_le
id └─────────┘ └─────┘ ┴ └────────┘ ┴ └────┘
src └─────────┘ └─────┘ └────────┘ └────┘
typ └─────────┘ └─────┘ ┴ └────────┘ ┴ └────┘
474
475 @[simp] theorem infi_true {s : true → α} : infi s = s trivial :=
id └──┘ ┴ └──┘ ┴ ┴ ┴ └─────┘
src └──┘ └──┘ ┴ └─────┘
typ └──┘ ┴ └──┘ ┴ ┴ ┴ └─────┘
doc └──┘ └──┘
476 le_antisymm (infi_le _ _) (le_infi $ assume ⟨⟩, le_refl _)
id └─────────┘ └─────┘ └─────┘ ┴ └─────┘
src └─────────┘ └─────┘ └─────┘ ┴ └─────┘
typ └─────────┘ └─────┘ └─────┘ ┴ └─────┘
477
478 @[simp] theorem supr_true {s : true → α} : supr s = s trivial :=
id └──┘ ┴ └──┘ ┴ ┴ ┴ └─────┘
src └──┘ └──┘ ┴ └─────┘
typ └──┘ ┴ └──┘ ┴ ┴ ┴ └─────┘
doc └──┘ └──┘
479 le_antisymm (supr_le $ assume ⟨⟩, le_refl _) (le_supr _ _)
id └─────────┘ └─────┘ ┴ └─────┘ └─────┘
src └─────────┘ └─────┘ ┴ └─────┘ └─────┘
typ └─────────┘ └─────┘ ┴ └─────┘ └─────┘
480
481 @[simp] theorem infi_exists {p : ι → Prop} {f : Exists p → α} : (⨅ x, f x) = (⨅ i, ⨅ h:p i, f ⟨i, h⟩) :=
id ┴ └────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └──┘ ┴ ┴ ┴ ┴ ┴ ┴
482 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
483 (le_infi $ assume i, le_infi $ assume : p i, infi_le _ _)
id └─────┘ ┴ └─────┘ ┴ ┴ └─────┘
src └─────┘ └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ ┴ └─────┘
484 (le_infi $ assume ⟨i, h⟩, infi_le_of_le i $ infi_le _ _)
id └─────┘ ┴┴ └───────────┘ └─────┘
src └─────┘ └───────────┘ └─────┘
typ └─────┘ ┴┴ └───────────┘ └─────┘
485
486 @[simp] theorem supr_exists {p : ι → Prop} {f : Exists p → α} : (⨆ x, f x) = (⨆ i, ⨆ h:p i, f ⟨i, h⟩) :=
id ┴ └────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └──┘ ┴ ┴ ┴ ┴ ┴ ┴
487 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
488 (supr_le $ assume ⟨i, h⟩, le_supr_of_le i $ le_supr (λh:p i, f ⟨i, h⟩) _)
id └─────┘ ┴┴ └───────────┘ └─────┘ ┴ ┴ ┴
src └─────┘ └───────────┘ └─────┘
typ └─────┘ ┴┴ └───────────┘ └─────┘ ┴ ┴ ┴
489 (supr_le $ assume i, supr_le $ assume : p i, le_supr _ _)
id └─────┘ ┴ └─────┘ ┴ ┴ └─────┘
src └─────┘ └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ ┴ └─────┘
490
491 theorem infi_and {p q : Prop} {s : p ∧ q → α} : infi s = (⨅ h₁ h₂, s ⟨h₁, h₂⟩) :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ └┘┴ ┴ └┘ └┘
src ┴ └──┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ └┘┴ ┴ └┘ └┘
doc └──┘ ┴ ┴
492 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
493 (le_infi $ assume i, le_infi $ assume j, infi_le _ _)
id └─────┘ ┴ └─────┘ ┴ └─────┘
src └─────┘ └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ └─────┘
494 (le_infi $ assume ⟨i, h⟩, infi_le_of_le i $ infi_le _ _)
id └─────┘ ┴┴ └───────────┘ └─────┘
src └─────┘ └───────────┘ └─────┘
typ └─────┘ ┴┴ └───────────┘ └─────┘
495
496 theorem supr_and {p q : Prop} {s : p ∧ q → α} : supr s = (⨆ h₁ h₂, s ⟨h₁, h₂⟩) :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ └┘┴ ┴ └┘ └┘
src ┴ └──┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ └┘┴ ┴ └┘ └┘
doc └──┘ ┴ ┴
497 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
498 (supr_le $ assume ⟨i, h⟩, le_supr_of_le i $ le_supr (λj, s ⟨i, j⟩) _)
id └─────┘ ┴┴ └───────────┘ └─────┘ ┴ ┴ ┴
src └─────┘ └───────────┘ └─────┘
typ └─────┘ ┴┴ └───────────┘ └─────┘ ┴ ┴ ┴
499 (supr_le $ assume i, supr_le $ assume j, le_supr _ _)
id └─────┘ ┴ └─────┘ ┴ └─────┘
src └─────┘ └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ └─────┘
500
501 theorem infi_or {p q : Prop} {s : p ∨ q → α} :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
502 infi s = (⨅ h : p, s (or.inl h)) ⊓ (⨅ h : q, s (or.inr h)) :=
id └──┘ ┴ ┴ ┴ ┴┴ ┴ └────┘ ┴ ┴ ┴ ┴┴ ┴ └────┘ ┴
src └──┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘
typ └──┘ ┴ ┴ ┴ ┴┴ ┴ └────┘ ┴ ┴ ┴ ┴┴ ┴ └────┘ ┴
doc └──┘ ┴ ┴ ┴ ┴
503 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
504 (le_inf
id └────┘
src └────┘
typ └────┘
505 (infi_le_infi2 $ assume j, ⟨_, le_refl _⟩)
id └───────────┘ ┴ └─────┘
src └───────────┘ └─────┘
typ └───────────┘ ┴ └─────┘
506 (infi_le_infi2 $ assume j, ⟨_, le_refl _⟩))
id └───────────┘ ┴ └─────┘
src └───────────┘ └─────┘
typ └───────────┘ ┴ └─────┘
507 (le_infi $ assume i, match i with
id └─────┘ ┴ ┴
src └─────┘
typ └─────┘ ┴ ┴
508 | or.inl i := inf_le_left_of_le $ infi_le _ _
id └────┘ └───────────────┘ └─────┘
src └────┘ └───────────────┘ └─────┘
typ └────┘ └───────────────┘ └─────┘
509 | or.inr j := inf_le_right_of_le $ infi_le _ _
id └────┘ └────────────────┘ └─────┘
src └────┘ └────────────────┘ └─────┘
typ └────┘ └────────────────┘ └─────┘
510 end)
511
512 theorem supr_or {p q : Prop} {s : p ∨ q → α} :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
513 (⨆ x, s x) = (⨆ i, s (or.inl i)) ⊔ (⨆ j, s (or.inr j)) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └────┘ ┴ ┴ ┴ ┴┴ ┴ └────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └────┘ ┴ ┴ ┴ ┴┴ ┴ └────┘ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
514 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
515 (supr_le $ assume s, match s with
id └─────┘ ┴ ┴
src └─────┘
typ └─────┘ ┴ ┴
516 | or.inl i := le_sup_left_of_le $ le_supr _ i
id └────┘ ┴ └───────────────┘ └─────┘
src └────┘ └───────────────┘ └─────┘
typ └────┘ ┴ └───────────────┘ └─────┘
517 | or.inr j := le_sup_right_of_le $ le_supr _ j
id └────┘ ┴ └────────────────┘ └─────┘
src └────┘ └────────────────┘ └─────┘
typ └────┘ ┴ └────────────────┘ └─────┘
518 end)
519 (sup_le
id └────┘
src └────┘
typ └────┘
520 (supr_le_supr2 $ assume i, ⟨or.inl i, le_refl _⟩)
id └───────────┘ ┴ └────┘ ┴ └─────┘
src └───────────┘ └────┘ └─────┘
typ └───────────┘ ┴ └────┘ ┴ └─────┘
521 (supr_le_supr2 $ assume j, ⟨or.inr j, le_refl _⟩))
id └───────────┘ ┴ └────┘ ┴ └─────┘
src └───────────┘ └────┘ └─────┘
typ └───────────┘ ┴ └────┘ ┴ └─────┘
522
523 theorem Inf_eq_infi {s : set α} : Inf s = (⨅a ∈ s, a) :=
id └─┘ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴
src └─┘ └─┘ ┴ ┴ ┴
typ └─┘ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴
doc └─┘ ┴ ┴
524 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
525 (le_infi $ assume b, le_infi $ assume h, Inf_le h)
id └─────┘ ┴ └─────┘ ┴ └────┘ ┴
src └─────┘ └─────┘ └────┘
typ └─────┘ ┴ └─────┘ ┴ └────┘ ┴
526 (le_Inf $ assume b h, infi_le_of_le b $ infi_le _ h)
id └────┘ ┴ ┴ └───────────┘ ┴ └─────┘ ┴
src └────┘ └───────────┘ └─────┘
typ └────┘ ┴ ┴ └───────────┘ ┴ └─────┘ ┴
527
528 theorem Sup_eq_supr {s : set α} : Sup s = (⨆a ∈ s, a) :=
id └─┘ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴
src └─┘ └─┘ ┴ ┴ ┴
typ └─┘ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴
doc └─┘ ┴ ┴
529 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
530 (Sup_le $ assume b h, le_supr_of_le b $ le_supr _ h)
id └────┘ ┴ ┴ └───────────┘ ┴ └─────┘ ┴
src └────┘ └───────────┘ └─────┘
typ └────┘ ┴ ┴ └───────────┘ ┴ └─────┘ ┴
531 (supr_le $ assume b, supr_le $ assume h, le_Sup h)
id └─────┘ ┴ └─────┘ ┴ └────┘ ┴
src └─────┘ └─────┘ └────┘
typ └─────┘ ┴ └─────┘ ┴ └────┘ ┴
532
533 lemma Sup_range {α : Type u} [has_Sup α] {f : ι → α} : Sup (range f) = supr f := rfl
id └─────┘ ┴ ┴ ┴ └─┘ └───┘ ┴ ┴ └──┘ ┴ └─┘
src └─────┘ └─┘ └───┘ ┴ └──┘ └─┘
typ └─────┘ ┴ ┴ ┴ └─┘ └───┘ ┴ ┴ └──┘ ┴ └─┘
doc └─────┘ └─┘ └───┘ └──┘
534
535 lemma Inf_range {α : Type u} [has_Inf α] {f : ι → α} : Inf (range f) = infi f := rfl
id └─────┘ ┴ ┴ ┴ └─┘ └───┘ ┴ ┴ └──┘ ┴ └─┘
src └─────┘ └─┘ └───┘ ┴ └──┘ └─┘
typ └─────┘ ┴ ┴ ┴ └─┘ └───┘ ┴ ┴ └──┘ ┴ └─┘
doc └─────┘ └─┘ └───┘ └──┘
536
537 lemma supr_range {g : β → α} {f : ι → β} : (⨆b∈range f, g b) = (⨆i, g (f i)) :=
id ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc ┴ └───┘ ┴ ┴ ┴
538 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
539 (supr_le $ assume b, supr_le $ assume ⟨i, (h : f i = b)⟩, h ▸ le_supr _ i)
id └─────┘ ┴ └─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src └─────┘ └─────┘ ┴ ┴ └─────┘
typ └─────┘ ┴ └─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └─────┘
540 (supr_le $ assume i, le_supr_of_le (f i) $ le_supr (λp, g (f i)) (mem_range_self _))
id └─────┘ ┴ └───────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └────────────┘
src └─────┘ └───────────┘ └─────┘ └────────────┘
typ └─────┘ ┴ └───────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └────────────┘
541
542 lemma infi_range {g : β → α} {f : ι → β} : (⨅b∈range f, g b) = (⨅i, g (f i)) :=
id ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc ┴ └───┘ ┴ ┴ ┴
543 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
544 (le_infi $ assume i, infi_le_of_le (f i) $ infi_le (λp, g (f i)) (mem_range_self _))
id └─────┘ ┴ └───────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └────────────┘
src └─────┘ └───────────┘ └─────┘ └────────────┘
typ └─────┘ ┴ └───────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └────────────┘
545 (le_infi $ assume b, le_infi $ assume ⟨i, (h : f i = b)⟩, h ▸ infi_le _ i)
id └─────┘ ┴ └─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src └─────┘ └─────┘ ┴ ┴ └─────┘
typ └─────┘ ┴ └─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └─────┘
546
547 theorem Inf_image {s : set β} {f : β → α} : Inf (f '' s) = (⨅ a ∈ s, f a) :=
id └─┘ ┴ ┴ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src └─┘ └─┘ └┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc └─┘ ┴ ┴
548 calc Inf (set.image f s) = (⨅a, ⨅h : ∃b, b ∈ s ∧ f b = a, a) : Inf_eq_infi
id └─┘ └───────┘ ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─────────┘
src └─┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘
typ └─┘ └───────┘ ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─────────┘
doc └─┘ ┴ ┴ ┴ ┴
549 ... = (⨅a, ⨅b, ⨅h : f b = a ∧ b ∈ s, a) : by simp [and_comm]
id ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └──────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└──────┘└─
typ ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └────┘└──────┘└─
doc ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────
550 ... = (⨅a, ⨅b, ⨅h : a = f b, ⨅h : b ∈ s, a) : by simp [infi_and, eq_comm]
id ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └──────┘ └─────┘
src ────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└──────┘└┘└─────┘└─
typ ────────────────────┘ ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └────┘└──────┘└┘└─────┘└─
doc ────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └┘ └─
txt ────────────────────┘ └────┘ └┘ └─
par ────────────────────┘ └────┘ └┘ └─
pid ────────────────────┘ ┴┴ └┘ ┴└
st ────────────────────┘ └─────────────────────────
551 ... = (⨅b, ⨅a, ⨅h : a = f b, ⨅h : b ∈ s, a) : by rw [infi_comm]
id ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └───────┘
src ────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└───────┘└─
typ ────────────────────┘ ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └──┘└───────┘└─
doc ────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─
txt ────────────────────┘ └──┘ └─
par ────────────────────┘ └──┘ └─
pid ────────────────────┘ └┘ ┴└
st ────────────────────┘ └────────────┘┴└
552 ... = (⨅a∈s, f a) : congr_arg infi $ by funext x; rw [infi_infi_eq_left]
id ┴┴ ┴┴ ┴ ┴ └───────┘ └──┘ └───────────────┘
src ────────────────────┘ ┴ ┴ └───────┘ └──┘ └──────┘ └──┘└───────────────┘└─
typ ────────────────────┘ ┴┴ ┴┴ ┴ ┴ └───────┘ └──┘ └──────┘ └──┘└───────────────┘└─
doc ────────────────────┘ ┴ ┴ └──┘ └──────┘ └──┘ └─
txt ────────────────────┘ └──────┘ └──┘ └─
par ────────────────────┘ └──────┘ └──┘ └─
pid ────────────────────┘ └┘ └┘ ┴└
st ────────────────────┘ └─────────────┘└───────────────┘┴└
553
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
554 theorem Sup_image {s : set β} {f : β → α} : Sup (f '' s) = (⨆ a ∈ s, f a) :=
id └─┘ ┴ ┴ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src └─┘ └─┘ └┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc └─┘ ┴ ┴
555 calc Sup (set.image f s) = (⨆a, ⨆h : ∃b, b ∈ s ∧ f b = a, a) : Sup_eq_supr
id └─┘ └───────┘ ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─────────┘
src └─┘ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘
typ └─┘ └───────┘ ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─────────┘
doc └─┘ ┴ ┴ ┴ ┴
556 ... = (⨆a, ⨆b, ⨆h : f b = a ∧ b ∈ s, a) : by simp [and_comm]
id ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └──────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└──────┘└─
typ ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └────┘└──────┘└─
doc ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────
557 ... = (⨆a, ⨆b, ⨆h : a = f b, ⨆h : b ∈ s, a) : by simp [supr_and, eq_comm]
id ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └──────┘ └─────┘
src ────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└──────┘└┘└─────┘└─
typ ────────────────────┘ ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └────┘└──────┘└┘└─────┘└─
doc ────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └┘ └─
txt ────────────────────┘ └────┘ └┘ └─
par ────────────────────┘ └────┘ └┘ └─
pid ────────────────────┘ ┴┴ └┘ ┴└
st ────────────────────┘ └─────────────────────────
558 ... = (⨆b, ⨆a, ⨆h : a = f b, ⨆h : b ∈ s, a) : by rw [supr_comm]
id ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └───────┘
src ────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└───────┘└─
typ ────────────────────┘ ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └──┘└───────┘└─
doc ────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └─
txt ────────────────────┘ └──┘ └─
par ────────────────────┘ └──┘ └─
pid ────────────────────┘ └┘ ┴└
st ────────────────────┘ └────────────┘┴└
559 ... = (⨆a∈s, f a) : congr_arg supr $ by funext x; rw [supr_supr_eq_left]
id ┴┴ ┴┴ ┴ ┴ └───────┘ └──┘ └───────────────┘
src ────────────────────┘ ┴ ┴ └───────┘ └──┘ └──────┘ └──┘└───────────────┘└─
typ ────────────────────┘ ┴┴ ┴┴ ┴ ┴ └───────┘ └──┘ └──────┘ └──┘└───────────────┘└─
doc ────────────────────┘ ┴ ┴ └──┘ └──────┘ └──┘ └─
txt ────────────────────┘ └──────┘ └──┘ └─
par ────────────────────┘ └──────┘ └──┘ └─
pid ────────────────────┘ └┘ └┘ ┴└
st ────────────────────┘ └─────────────┘└───────────────┘┴└
560
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
561 /- supr and infi under set constructions -/
src ────────────────────────────────────────────
typ ────────────────────────────────────────────
doc ────────────────────────────────────────────
txt ────────────────────────────────────────────
par ────────────────────────────────────────────
pid ────────────────────────────────────────────
st ────────────────────────────────────────────
562
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
563 /- should work using the simplifier! -/
src ───────────────────────────────────────┘
typ ───────────────────────────────────────┘
doc ───────────────────────────────────────┘
txt ───────────────────────────────────────┘
par ───────────────────────────────────────┘
pid ───────────────────────────────────────┘
st ───────────────────────────────────────┘
564 @[simp] theorem infi_emptyset {f : β → α} : (⨅ x ∈ (∅ : set β), f x) = ⊤ :=
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
565 le_antisymm le_top (le_infi $ assume x, le_infi false.elim)
id └─────────┘ └────┘ └─────┘ ┴ └─────┘ └────────┘
src └─────────┘ └────┘ └─────┘ └─────┘ └────────┘
typ └─────────┘ └────┘ └─────┘ ┴ └─────┘ └────────┘
566
567 @[simp] theorem supr_emptyset {f : β → α} : (⨆ x ∈ (∅ : set β), f x) = ⊥ :=
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
568 le_antisymm (supr_le $ assume x, supr_le false.elim) bot_le
id └─────────┘ └─────┘ ┴ └─────┘ └────────┘ └────┘
src └─────────┘ └─────┘ └─────┘ └────────┘ └────┘
typ └─────────┘ └─────┘ ┴ └─────┘ └────────┘ └────┘
569
570 @[simp] theorem infi_univ {f : β → α} : (⨅ x ∈ (univ : set β), f x) = (⨅ x, f x) :=
id ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ └──┘ └─┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc └──┘ ┴ ┴ ┴ ┴
571 show (⨅ (x : β) (H : true), f x) = ⨅ (x : β), f x,
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
572 from congr_arg infi $ funext $ assume x, infi_const
id └───────┘ └──┘ └────┘ ┴ └────────┘
src └───────┘ └──┘ └────┘ └────────┘
typ └───────┘ └──┘ └────┘ ┴ └────────┘
doc └──┘
573
574 @[simp] theorem supr_univ {f : β → α} : (⨆ x ∈ (univ : set β), f x) = (⨆ x, f x) :=
id ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ └──┘ └─┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc └──┘ ┴ ┴ ┴ ┴
575 show (⨆ (x : β) (H : true), f x) = ⨆ (x : β), f x,
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
576 from congr_arg supr $ funext $ assume x, supr_const
id └───────┘ └──┘ └────┘ ┴ └────────┘
src └───────┘ └──┘ └────┘ └────────┘
typ └───────┘ └──┘ └────┘ ┴ └────────┘
doc └──┘
577
578 @[simp] theorem infi_union {f : β → α} {s t : set β} : (⨅ x ∈ s ∪ t, f x) = (⨅x∈s, f x) ⊓ (⨅x∈t, f x) :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
doc └──┘ ┴ ┴ ┴ ┴ ┴ ┴
579 calc (⨅ x ∈ s ∪ t, f x) = (⨅ x, (⨅h : x∈s, f x) ⊓ (⨅h : x∈t, f x)) : congr_arg infi $ funext $ assume x, infi_or
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴┴ ┴ ┴ └───────┘ └──┘ └────┘ ┴ └─────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └──┘ └────┘ └─────┘
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴┴ ┴ ┴ └───────┘ └──┘ └────┘ ┴ └─────┘
doc ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
580 ... = (⨅x∈s, f x) ⊓ (⨅x∈t, f x) : infi_inf_eq
id ┴┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ └─────────┘
src ┴ ┴ ┴ ┴ ┴ └─────────┘
typ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ └─────────┘
doc ┴ ┴ ┴ ┴
581
582 theorem infi_le_infi_of_subset {f : β → α} {s t : set β} (h : s ⊆ t) :
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
583 (⨅ x ∈ t, f x) ≤ (⨅ x ∈ s, f x) :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴
584 by rw [(union_eq_self_of_subset_left h).symm, infi_union]; exact inf_le_left
id └──────────────────────────┘ ┴ └────────┘ └─────────┘
src └──┘ └──────────────────────────┘┴ └──────┘└────────┘┴ └────┘└─────────┘└
typ └──┘ └──────────────────────────┘┴┴└──────┘└────────┘┴ └────┘└─────────┘└
doc └──┘ ┴ └──────┘ ┴ └────┘ └
txt └──┘ ┴ └──────┘ ┴ └────┘ └
par └──┘ ┴ └──────┘ ┴ └────┘ └
pid └┘ ┴ └──────┘ ┴ ┴ └
st └───────────────────────────────────────┘└───────────┘┴└───────────────────
585
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
586 @[simp] theorem supr_union {f : β → α} {s t : set β} : (⨆ x ∈ s ∪ t, f x) = (⨆x∈s, f x) ⊔ (⨆x∈t, f x) :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
doc └──┘ ┴ ┴ ┴ ┴ ┴ ┴
587 calc (⨆ x ∈ s ∪ t, f x) = (⨆ x, (⨆h : x∈s, f x) ⊔ (⨆h : x∈t, f x)) : congr_arg supr $ funext $ assume x, supr_or
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴┴ ┴ ┴ └───────┘ └──┘ └────┘ ┴ └─────┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └──┘ └────┘ └─────┘
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴┴ ┴ ┴ └───────┘ └──┘ └────┘ ┴ └─────┘
doc ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
588 ... = (⨆x∈s, f x) ⊔ (⨆x∈t, f x) : supr_sup_eq
id ┴┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ └─────────┘
src ┴ ┴ ┴ ┴ ┴ └─────────┘
typ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ └─────────┘
doc ┴ ┴ ┴ ┴
589
590 theorem supr_le_supr_of_subset {f : β → α} {s t : set β} (h : s ⊆ t) :
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
591 (⨆ x ∈ s, f x) ≤ (⨆ x ∈ t, f x) :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴
592 by rw [(union_eq_self_of_subset_left h).symm, supr_union]; exact le_sup_left
id └──────────────────────────┘ ┴ └────────┘ └─────────┘
src └──┘ └──────────────────────────┘┴ └──────┘└────────┘┴ └────┘└─────────┘└
typ └──┘ └──────────────────────────┘┴┴└──────┘└────────┘┴ └────┘└─────────┘└
doc └──┘ ┴ └──────┘ ┴ └────┘ └
txt └──┘ ┴ └──────┘ ┴ └────┘ └
par └──┘ ┴ └──────┘ ┴ └────┘ └
pid └┘ ┴ └──────┘ ┴ ┴ └
st └───────────────────────────────────────┘└───────────┘┴└───────────────────
593
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
594 @[simp] theorem insert_of_has_insert {α : Type*} (x : α) (a : set α) :
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
doc └──┘
595 has_insert.insert x a = insert x a := rfl
id └───────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘
src └───────────────┘ ┴ └────┘ └─┘
typ └───────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘
596
597 @[simp] theorem infi_insert {f : β → α} {s : set β} {b : β} : (⨅ x ∈ insert b s, f x) = f b ⊓ (⨅x∈s, f x) :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
src └─┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
doc └──┘ ┴ ┴ ┴ ┴
598 eq.trans infi_union $ congr_arg (λx:α, x ⊓ (⨅x∈s, f x)) infi_infi_eq_left
id └──────┘ └────────┘ └───────┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ └───────────────┘
src └──────┘ └────────┘ └───────┘ ┴ ┴ ┴ └───────────────┘
typ └──────┘ └────────┘ └───────┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ └───────────────┘
doc ┴ ┴
599
600 @[simp] theorem supr_insert {f : β → α} {s : set β} {b : β} : (⨆ x ∈ insert b s, f x) = f b ⊔ (⨆x∈s, f x) :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
src └─┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
doc └──┘ ┴ ┴ ┴ ┴
601 eq.trans supr_union $ congr_arg (λx:α, x ⊔ (⨆x∈s, f x)) supr_supr_eq_left
id └──────┘ └────────┘ └───────┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ └───────────────┘
src └──────┘ └────────┘ └───────┘ ┴ ┴ ┴ └───────────────┘
typ └──────┘ └────────┘ └───────┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ └───────────────┘
doc ┴ ┴
602
603 @[simp] theorem infi_singleton {f : β → α} {b : β} : (⨅ x ∈ (singleton b : set β), f x) = f b :=
id ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───────┘ └─┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
604 show (⨅ x ∈ insert b (∅ : set β), f x) = f b,
id ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └────┘ ┴ └─┘ ┴ ┴
typ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
605 by simp
src └────
typ └────
doc └────
txt └────
par └────
pid └
st └─────
606
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
607 @[simp] theorem infi_pair {f : β → α} {a b : β} : (⨅ x ∈ ({a, b} : set β), f x) = f a ⊓ f b :=
id ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
608 by { rw [show {a, b} = (insert b {a} : set β), from rfl, infi_insert, inf_comm], simp }
id ┴ └────┘ ┴ ┴ └─┘ ┴ └─┘ └─────────┘ └──────┘
src └──┘ ┴ └─┘ └┘┴┴ └────┘┴ ┴┴└───┘└─┘┴ └──────┘└─┘└┘└─────────┘└┘└──────┘┴ └───┘
typ └──┘ ┴ └─┘ └┘┴┴ └────┘┴┴┴┴└───┘└─┘┴┴└──────┘└─┘└┘└─────────┘└┘└──────┘┴ └───┘
doc └──┘ ┴ └─┘ └┘ ┴ ┴ ┴ └───┘ ┴ └──────┘ └┘ └┘ ┴ └───┘
txt └──┘ ┴ └─┘ └┘ ┴ ┴ ┴ └───┘ ┴ └──────┘ └┘ └┘ ┴ └───┘
par └──┘ ┴ └─┘ └┘ ┴ ┴ ┴ └───┘ ┴ └──────┘ └┘ └┘ ┴ └───┘
pid └┘ ┴ └─┘ └┘ ┴ ┴ ┴ └───┘ ┴ └──────┘ └┘ └┘ ┴ ┴
st └───────────────────────────────────────────────────┘└───────────┘└────────┘└──────┘└┘
609
610 @[simp] theorem supr_singleton {f : β → α} {b : β} : (⨆ x ∈ (singleton b : set β), f x) = f b :=
id ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───────┘ └─┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
611 show (⨆ x ∈ insert b (∅ : set β), f x) = f b,
id ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └────┘ ┴ └─┘ ┴ ┴
typ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
612 by simp
src └────
typ └────
doc └────
txt └────
par └────
pid └
st └─────
613
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
614 @[simp] theorem supr_pair {f : β → α} {a b : β} : (⨆ x ∈ ({a, b} : set β), f x) = f a ⊔ f b :=
id ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
615 by { rw [show {a, b} = (insert b {a} : set β), from rfl, supr_insert, sup_comm], simp }
id ┴ └────┘ ┴ ┴ └─┘ ┴ └─┘ └─────────┘ └──────┘
src └──┘ ┴ └─┘ └┘┴┴ └────┘┴ ┴┴└───┘└─┘┴ └──────┘└─┘└┘└─────────┘└┘└──────┘┴ └───┘
typ └──┘ ┴ └─┘ └┘┴┴ └────┘┴┴┴┴└───┘└─┘┴┴└──────┘└─┘└┘└─────────┘└┘└──────┘┴ └───┘
doc └──┘ ┴ └─┘ └┘ ┴ ┴ ┴ └───┘ ┴ └──────┘ └┘ └┘ ┴ └───┘
txt └──┘ ┴ └─┘ └┘ ┴ ┴ ┴ └───┘ ┴ └──────┘ └┘ └┘ ┴ └───┘
par └──┘ ┴ └─┘ └┘ ┴ ┴ ┴ └───┘ ┴ └──────┘ └┘ └┘ ┴ └───┘
pid └┘ ┴ └─┘ └┘ ┴ ┴ ┴ └───┘ ┴ └──────┘ └┘ └┘ ┴ ┴
st └───────────────────────────────────────────────────┘└───────────┘└────────┘└──────┘└┘
616
617 lemma infi_image {γ} {f : β → γ} {g : γ → α} {t : set β} :
id ┴ ┴ ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ ┴ ┴ └─┘ ┴
618 (⨅ c ∈ f '' t, g c) = (⨅ b ∈ t, g (f b)) :=
id ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ └┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
619 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
620 (le_infi $ assume b, le_infi $ assume hbt,
id └─────┘ ┴ └─────┘ └─┘
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ └─┘
621 infi_le_of_le (f b) $ infi_le (λ_, g (f b)) (mem_image_of_mem f hbt))
id └───────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └──────────────┘ ┴ └─┘
src └───────────┘ └─────┘ └──────────────┘
typ └───────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └──────────────┘ ┴ └─┘
622 (le_infi $ assume c, le_infi $ assume ⟨b, hbt, eq⟩,
id └─────┘ ┴ └─────┘ ┴┴ └─┘ └┘
src └─────┘ └─────┘ └┘
typ └─────┘ ┴ └─────┘ ┴┴ └─┘ └┘
623 eq ▸ infi_le_of_le b $ infi_le (λ_, g (f b)) hbt)
id ┴ └───────────┘ └─────┘ ┴ ┴ ┴
src ┴ └───────────┘ └─────┘
typ ┴ └───────────┘ └─────┘ ┴ ┴ ┴
624
625 lemma supr_image {γ} {f : β → γ} {g : γ → α} {t : set β} :
id ┴ ┴ ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ ┴ ┴ └─┘ ┴
626 (⨆ c ∈ f '' t, g c) = (⨆ b ∈ t, g (f b)) :=
id ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ └┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
627 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
628 (supr_le $ assume c, supr_le $ assume ⟨b, hbt, eq⟩,
id └─────┘ ┴ └─────┘ ┴┴ └─┘ └┘
src └─────┘ └─────┘ └┘
typ └─────┘ ┴ └─────┘ ┴┴ └─┘ └┘
629 eq ▸ le_supr_of_le b $ le_supr (λ_, g (f b)) hbt)
id ┴ └───────────┘ └─────┘ ┴ ┴ ┴
src ┴ └───────────┘ └─────┘
typ ┴ └───────────┘ └─────┘ ┴ ┴ ┴
630 (supr_le $ assume b, supr_le $ assume hbt,
id └─────┘ ┴ └─────┘ └─┘
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ └─┘
631 le_supr_of_le (f b) $ le_supr (λ_, g (f b)) (mem_image_of_mem f hbt))
id └───────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └──────────────┘ ┴ └─┘
src └───────────┘ └─────┘ └──────────────┘
typ └───────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └──────────────┘ ┴ └─┘
632
633 /- supr and infi under Type -/
634
635 @[simp] theorem infi_empty {s : empty → α} : infi s = ⊤ :=
id └───┘ ┴ └──┘ ┴ ┴ ┴
src └───┘ └──┘ ┴ ┴
typ └───┘ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
636 le_antisymm le_top (le_infi $ assume i, empty.rec_on _ i)
id └─────────┘ └────┘ └─────┘ ┴ └──────────┘ ┴
src └─────────┘ └────┘ └─────┘ └──────────┘
typ └─────────┘ └────┘ └─────┘ ┴ └──────────┘ ┴
637
638 @[simp] theorem supr_empty {s : empty → α} : supr s = ⊥ :=
id └───┘ ┴ └──┘ ┴ ┴ ┴
src └───┘ └──┘ ┴ ┴
typ └───┘ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
639 le_antisymm (supr_le $ assume i, empty.rec_on _ i) bot_le
id └─────────┘ └─────┘ ┴ └──────────┘ ┴ └────┘
src └─────────┘ └─────┘ └──────────┘ └────┘
typ └─────────┘ └─────┘ ┴ └──────────┘ ┴ └────┘
640
641 @[simp] theorem infi_unit {f : unit → α} : (⨅ x, f x) = f () :=
id └──┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘
src └──┘ ┴ ┴ ┴ └┘
typ └──┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘
doc └──┘ └──┘ ┴ ┴
642 le_antisymm (infi_le _ _) (le_infi $ assume ⟨⟩, le_refl _)
id └─────────┘ └─────┘ └─────┘ ┴ └─────┘
src └─────────┘ └─────┘ └─────┘ ┴ └─────┘
typ └─────────┘ └─────┘ └─────┘ ┴ └─────┘
643
644 @[simp] theorem supr_unit {f : unit → α} : (⨆ x, f x) = f () :=
id └──┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘
src └──┘ ┴ ┴ ┴ └┘
typ └──┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘
doc └──┘ └──┘ ┴ ┴
645 le_antisymm (supr_le $ assume ⟨⟩, le_refl _) (le_supr _ _)
id └─────────┘ └─────┘ ┴ └─────┘ └─────┘
src └─────────┘ └─────┘ ┴ └─────┘ └─────┘
typ └─────────┘ └─────┘ ┴ └─────┘ └─────┘
646
647 lemma supr_bool_eq {f : bool → α} : (⨆b:bool, f b) = f tt ⊔ f ff :=
id └──┘ ┴ ┴ └──┘┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
src └──┘ ┴ └──┘┴ ┴ └┘ ┴ └┘
typ └──┘ ┴ ┴ └──┘┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
doc ┴ ┴
648 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
649 (supr_le $ assume b, match b with tt := le_sup_left | ff := le_sup_right end)
id └─────┘ ┴ ┴ └┘ └─────────┘ └┘ └──────────┘
src └─────┘ └┘ └─────────┘ └┘ └──────────┘
typ └─────┘ ┴ ┴ └┘ └─────────┘ └┘ └──────────┘
650 (sup_le (le_supr _ _) (le_supr _ _))
id └────┘ └─────┘ └─────┘
src └────┘ └─────┘ └─────┘
typ └────┘ └─────┘ └─────┘
651
652 lemma infi_bool_eq {f : bool → α} : (⨅b:bool, f b) = f tt ⊓ f ff :=
id └──┘ ┴ ┴ └──┘┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
src └──┘ ┴ └──┘┴ ┴ └┘ ┴ └┘
typ └──┘ ┴ ┴ └──┘┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
doc ┴ ┴
653 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
654 (le_inf (infi_le _ _) (infi_le _ _))
id └────┘ └─────┘ └─────┘
src └────┘ └─────┘ └─────┘
typ └────┘ └─────┘ └─────┘
655 (le_infi $ assume b, match b with tt := inf_le_left | ff := inf_le_right end)
id └─────┘ ┴ ┴ └┘ └─────────┘ └┘ └──────────┘
src └─────┘ └┘ └─────────┘ └┘ └──────────┘
typ └─────┘ ┴ ┴ └┘ └─────────┘ └┘ └──────────┘
656
657 theorem infi_subtype {p : ι → Prop} {f : subtype p → α} : (⨅ x, f x) = (⨅ i (h:p i), f ⟨i, h⟩) :=
id ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
658 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
659 (le_infi $ assume i, le_infi $ assume : p i, infi_le _ _)
id └─────┘ ┴ └─────┘ ┴ ┴ └─────┘
src └─────┘ └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ ┴ └─────┘
660 (le_infi $ assume ⟨i, h⟩, infi_le_of_le i $ infi_le _ _)
id └─────┘ ┴┴ └───────────┘ └─────┘
src └─────┘ └───────────┘ └─────┘
typ └─────┘ ┴┴ └───────────┘ └─────┘
661
662 lemma infi_subtype' {p : ι → Prop} {f : ∀ i, p i → α} :
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
663 (⨅ i (h : p i), f i h) = (⨅ x : subtype p, f x.val x.property) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴┴ ┴ ┴└──┘ ┴└───────┘
src ┴ ┴ ┴ ┴ └─────┘ ┴ └──┘ └───────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴┴ ┴ ┴└──┘ ┴└───────┘
doc ┴ ┴ ┴ ┴
664 (@infi_subtype _ _ _ p (λ x, f x.val x.property)).symm
id └──────────┘ ┴ ┴ ┴ ┴└──┘ ┴└───────┘ └──┘
src └──────────┘ └──┘ └───────┘ └──┘
typ └──────────┘ ┴ ┴ ┴ ┴└──┘ ┴└───────┘ └──┘
665
666 theorem supr_subtype {p : ι → Prop} {f : subtype p → α} : (⨆ x, f x) = (⨆ i (h:p i), f ⟨i, h⟩) :=
id ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
667 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
668 (supr_le $ assume ⟨i, h⟩, le_supr_of_le i $ le_supr (λh:p i, f ⟨i, h⟩) _)
id └─────┘ ┴┴ └───────────┘ └─────┘ ┴ ┴ ┴
src └─────┘ └───────────┘ └─────┘
typ └─────┘ ┴┴ └───────────┘ └─────┘ ┴ ┴ ┴
669 (supr_le $ assume i, supr_le $ assume : p i, le_supr _ _)
id └─────┘ ┴ └─────┘ ┴ ┴ └─────┘
src └─────┘ └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ ┴ └─────┘
670
671 theorem infi_sigma {p : β → Type w} {f : sigma p → α} : (⨅ x, f x) = (⨅ i (h:p i), f ⟨i, h⟩) :=
id ┴ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
672 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
673 (le_infi $ assume i, le_infi $ assume : p i, infi_le _ _)
id └─────┘ ┴ └─────┘ ┴ ┴ └─────┘
src └─────┘ └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ ┴ └─────┘
674 (le_infi $ assume ⟨i, h⟩, infi_le_of_le i $ infi_le _ _)
id └─────┘ ┴┴ └───────────┘ └─────┘
src └─────┘ └───────────┘ └─────┘
typ └─────┘ ┴┴ └───────────┘ └─────┘
675
676 theorem supr_sigma {p : β → Type w} {f : sigma p → α} : (⨆ x, f x) = (⨆ i (h:p i), f ⟨i, h⟩) :=
id ┴ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
677 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
678 (supr_le $ assume ⟨i, h⟩, le_supr_of_le i $ le_supr (λh:p i, f ⟨i, h⟩) _)
id └─────┘ ┴┴ └───────────┘ └─────┘ ┴ ┴ ┴
src └─────┘ └───────────┘ └─────┘
typ └─────┘ ┴┴ └───────────┘ └─────┘ ┴ ┴ ┴
679 (supr_le $ assume i, supr_le $ assume : p i, le_supr _ _)
id └─────┘ ┴ └─────┘ ┴ ┴ └─────┘
src └─────┘ └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ ┴ └─────┘
680
681 theorem infi_prod {γ : Type w} {f : β × γ → α} : (⨅ x, f x) = (⨅ i j, f (i, j)) :=
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴
doc ┴ ┴ ┴ ┴
682 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
683 (le_infi $ assume i, le_infi $ assume j, infi_le _ _)
id └─────┘ ┴ └─────┘ ┴ └─────┘
src └─────┘ └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ └─────┘
684 (le_infi $ assume ⟨i, h⟩, infi_le_of_le i $ infi_le _ _)
id └─────┘ ┴┴ └───────────┘ └─────┘
src └─────┘ └───────────┘ └─────┘
typ └─────┘ ┴┴ └───────────┘ └─────┘
685
686 theorem supr_prod {γ : Type w} {f : β × γ → α} : (⨆ x, f x) = (⨆ i j, f (i, j)) :=
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴
doc ┴ ┴ ┴ ┴
687 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
688 (supr_le $ assume ⟨i, h⟩, le_supr_of_le i $ le_supr (λj, f ⟨i, j⟩) _)
id └─────┘ ┴┴ └───────────┘ └─────┘ ┴ ┴ ┴
src └─────┘ └───────────┘ └─────┘
typ └─────┘ ┴┴ └───────────┘ └─────┘ ┴ ┴ ┴
689 (supr_le $ assume i, supr_le $ assume j, le_supr _ _)
id └─────┘ ┴ └─────┘ ┴ └─────┘
src └─────┘ └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ └─────┘
690
691 theorem infi_sum {γ : Type w} {f : β ⊕ γ → α} :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
692 (⨅ x, f x) = (⨅ i, f (sum.inl i)) ⊓ (⨅ j, f (sum.inr j)) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ └─────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ └─────┘ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
693 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
694 (le_inf
id └────┘
src └────┘
typ └────┘
695 (infi_le_infi2 $ assume i, ⟨_, le_refl _⟩)
id └───────────┘ ┴ └─────┘
src └───────────┘ └─────┘
typ └───────────┘ ┴ └─────┘
696 (infi_le_infi2 $ assume j, ⟨_, le_refl _⟩))
id └───────────┘ ┴ └─────┘
src └───────────┘ └─────┘
typ └───────────┘ ┴ └─────┘
697 (le_infi $ assume s, match s with
id └─────┘ ┴ ┴
src └─────┘
typ └─────┘ ┴ ┴
698 | sum.inl i := inf_le_left_of_le $ infi_le _ _
id └─────┘ └───────────────┘ └─────┘
src └─────┘ └───────────────┘ └─────┘
typ └─────┘ └───────────────┘ └─────┘
699 | sum.inr j := inf_le_right_of_le $ infi_le _ _
id └─────┘ └────────────────┘ └─────┘
src └─────┘ └────────────────┘ └─────┘
typ └─────┘ └────────────────┘ └─────┘
700 end)
701
702 theorem supr_sum {γ : Type w} {f : β ⊕ γ → α} :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
703 (⨆ x, f x) = (⨆ i, f (sum.inl i)) ⊔ (⨆ j, f (sum.inr j)) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ └─────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ └─────┘ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
704 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
705 (supr_le $ assume s, match s with
id └─────┘ ┴ ┴
src └─────┘
typ └─────┘ ┴ ┴
706 | sum.inl i := le_sup_left_of_le $ le_supr _ i
id └─────┘ ┴ └───────────────┘ └─────┘
src └─────┘ └───────────────┘ └─────┘
typ └─────┘ ┴ └───────────────┘ └─────┘
707 | sum.inr j := le_sup_right_of_le $ le_supr _ j
id └─────┘ ┴ └────────────────┘ └─────┘
src └─────┘ └────────────────┘ └─────┘
typ └─────┘ ┴ └────────────────┘ └─────┘
708 end)
709 (sup_le
id └────┘
src └────┘
typ └────┘
710 (supr_le_supr2 $ assume i, ⟨sum.inl i, le_refl _⟩)
id └───────────┘ ┴ └─────┘ ┴ └─────┘
src └───────────┘ └─────┘ └─────┘
typ └───────────┘ ┴ └─────┘ ┴ └─────┘
711 (supr_le_supr2 $ assume j, ⟨sum.inr j, le_refl _⟩))
id └───────────┘ ┴ └─────┘ ┴ └─────┘
src └───────────┘ └─────┘ └─────┘
typ └───────────┘ ┴ └─────┘ ┴ └─────┘
712
713 end
714
715 section complete_linear_order
716 variables [complete_linear_order α]
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
doc └───────────────────┘
717
718 lemma supr_eq_top (f : ι → α) : supr f = ⊤ ↔ (∀b<⊤, ∃i, b < f i) :=
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
doc └──┘
719 by rw [← Sup_range, Sup_eq_top];
id └───────┘ └────────┘
src └────┘└───────┘└┘└────────┘┴
typ └────┘└───────┘└┘└────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid └──┘ └┘ ┴
st └──────────────┘└──────────┘┴└─
720 from forall_congr (assume b, forall_congr (assume hb, set.exists_range_iff))
id └──────────┘ └──────────────────┘
src └───┘ ┴ └──┘└──────────┘┴ └───┘└──────────────────┘└──
typ └───┘ ┴ └──┘└──────────┘┴ └───┘└──────────────────┘└──
doc └───┘ ┴ └──┘ ┴ └───┘ └──
txt └───┘ ┴ └──┘ ┴ └───┘ └──
par └───┘ ┴ └──┘ ┴ └───┘ └──
pid └───┘ ┴ └──┘ ┴ └───┘ └┘└
st ─────────────────────────────────────────────────────────────────────────────
721
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
722 lemma infi_eq_bot (f : ι → α) : infi f = ⊥ ↔ (∀b>⊥, ∃i, b > f i) :=
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
doc └──┘
723 by rw [← Inf_range, Inf_eq_bot];
id └───────┘ └────────┘
src └────┘└───────┘└┘└────────┘┴
typ └────┘└───────┘└┘└────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid └──┘ └┘ ┴
st └──────────────┘└──────────┘┴└─
724 from forall_congr (assume b, forall_congr (assume hb, set.exists_range_iff))
id └──────────┘ └──────────────────┘
src └───┘ ┴ └──┘└──────────┘┴ └───┘└──────────────────┘└──
typ └───┘ ┴ └──┘└──────────┘┴ └───┘└──────────────────┘└──
doc └───┘ ┴ └──┘ ┴ └───┘ └──
txt └───┘ ┴ └──┘ ┴ └───┘ └──
par └───┘ ┴ └──┘ ┴ └───┘ └──
pid └───┘ ┴ └──┘ ┴ └───┘ └┘└
st ─────────────────────────────────────────────────────────────────────────────
725
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
726 end complete_linear_order
727
728 /- Instances -/
729
730 instance complete_lattice_Prop : complete_lattice Prop :=
id └──────────────┘
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
731 { Sup := λs, ∃a∈s, a,
id ┴ ┴┴ ┴┴ ┴
src ┴ ┴
typ ┴ ┴┴ ┴┴ ┴
732 le_Sup := assume s a h p, ⟨a, h, p⟩,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
733 Sup_le := assume s a h ⟨b, h', p⟩, h b h' p,
id ┴ ┴ ┴ ┴ └┘ ┴ ┴
typ ┴ ┴ ┴ ┴ └┘ ┴ ┴
734 Inf := λs, ∀a:Prop, a∈s → a,
id ┴ └──┘ ┴┴┴ ┴
src ┴
typ ┴ └──┘ ┴┴┴ ┴
735 Inf_le := assume s a h p, p a h,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
736 le_Inf := assume s a h p b hb, h b hb p,
id ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
737 ..lattice.bounded_lattice_Prop }
id └──────────────────────────┘
src └──────────────────────────┘
typ └──────────────────────────┘
738
739 lemma Inf_Prop_eq {s : set Prop} : Inf s = (∀p ∈ s, p) := rfl
id └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘
src └─┘ └─┘ ┴ └─┘
typ └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘
doc └─┘
740
741 lemma Sup_Prop_eq {s : set Prop} : Sup s = (∃p ∈ s, p) := rfl
id └─┘ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ └─┘
src └─┘ └─┘ ┴ ┴ ┴ └─┘
typ └─┘ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ └─┘
doc └─┘
742
743 lemma infi_Prop_eq {ι : Sort*} {p : ι → Prop} : (⨅i, p i) = (∀i, p i) :=
id ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
744 le_antisymm (assume h i, h _ ⟨i, rfl⟩ ) (assume h p ⟨i, eq⟩, eq ▸ h i)
id └─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴ └┘ ┴ ┴
src └─────────┘ └─┘ └┘ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴ └┘ ┴ ┴
745
746 lemma supr_Prop_eq {ι : Sort*} {p : ι → Prop} : (⨆i, p i) = (∃i, p i) :=
id ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc ┴ ┴
747 le_antisymm (assume ⟨q, ⟨i, (eq : p i = q)⟩, hq⟩, ⟨i, eq.symm ▸ hq⟩) (assume ⟨i, hi⟩, ⟨p i, ⟨i, rfl⟩, hi⟩)
id └─────────┘ ┴ ┴ ┴ ┴ ┴ └┘ └───┘ ┴ ┴┴ └┘ ┴ └─┘
src └─────────┘ ┴ ┴ └───┘ ┴ └─┘
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ └┘ └───┘ ┴ ┴┴ └┘ ┴ └─┘
748
749 instance pi.complete_lattice {α : Type u} {β : α → Type v} [∀ i, complete_lattice (β i)] :
id ┴ ┴ └──────────────┘ ┴ ┴
src └──────────────┘
typ ┴ ┴ └──────────────┘ ┴ ┴
doc └──────────────┘
750 complete_lattice (Π i, β i) :=
id └──────────────┘ ┴ ┴ ┴
src └──────────────┘
typ └──────────────┘ ┴ ┴ ┴
doc └──────────────┘
751 by { pi_instance;
src └─────────┘
typ └─────────┘
txt └─────────┘
par └─────────┘
st └───────────────
752 { intros, intro,
src └────┘ └───┘
typ └────┘ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
st ────┘└──────┘└─────┘└─
753 apply_field, intros,
src └─────────┘ └────┘
typ └─────────┘ └────┘
doc └─────────┘ └────┘
txt └─────────┘ └────┘
par └─────────┘ └────┘
st ─────────────────┘└──────┘└─
754 simp at H, rcases H with ⟨ x, H₀, H₁ ⟩,
id ┴
src └───────┘ └─────┘ └─────────────────┘
typ └───────┘ └─────┘┴└─────────────────┘
doc └───────┘ └─────┘ └─────────────────┘
txt └───────┘ └─────┘ └─────────────────┘
par └───────┘ └─────┘ └─────────────────┘
pid ┴└──┘ ┴ └─────────────────┘
st ───────────────┘└───────────────────────────┘└─
755 subst b, apply a_1 _ H₀ i, } }
id ┴ └─┘ └┘ ┴
src └────┘ └────┘ └─┘ ┴
typ └────┘┴ └────┘└─┘└─┘└┘┴┴
doc └────┘ └────┘ └─┘ ┴
txt └────┘ └────┘ └─┘ ┴
par └────┘ └────┘ └─┘ ┴
pid ┴ ┴ └─┘ ┴
st ─────────────┘└────────────────┘└────┘
756
757 lemma Inf_apply
758 {α : Type u} {β : α → Type v} [∀ i, complete_lattice (β i)] {s : set (Πa, β a)} {a : α} :
id ┴ ┴ └──────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └──────────────┘ └─┘
typ ┴ ┴ └──────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
doc └──────────────┘
759 (Inf s) a = (⨅f∈s, (f : Πa, β a) a) :=
id └─┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └─┘ ┴ ┴
760 by rw [← Inf_image]; refl
id └───────┘
src └────┘└───────┘┴ └────
typ └────┘└───────┘┴ └────
doc └────┘ ┴ └────
txt └────┘ ┴ └────
par └────┘ ┴ └────
pid └──┘ ┴ └
st └──────────────┘┴└──────
761
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
762 lemma infi_apply {α : Type u} {β : α → Type v} {ι : Sort*} [∀ i, complete_lattice (β i)]
id ┴ ┴ └──────────────┘ ┴ ┴
src └──────────────┘
typ ┴ ┴ └──────────────┘ ┴ ┴
doc └──────────────┘
763 {f : ι → Πa, β a} {a : α} : (⨅i, f i) a = (⨅i, f i a) :=
id ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
764 by erw [← Inf_range, Inf_apply, infi_range]
id └───────┘ └───────┘ └────────┘
src └─────┘└───────┘└┘└───────┘└┘└────────┘└─
typ └─────┘└───────┘└┘└───────┘└┘└────────┘└─
doc └─────┘ └┘ └┘ └─
txt └─────┘ └┘ └┘ └─
par └─────┘ └┘ └┘ └─
pid └──┘ └┘ └┘ ┴└
st └───────────────┘└─────────┘└──────────┘┴└
765
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
766 lemma Sup_apply
767 {α : Type u} {β : α → Type v} [∀ i, complete_lattice (β i)] {s : set (Πa, β a)} {a : α} :
id ┴ ┴ └──────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └──────────────┘ └─┘
typ ┴ ┴ └──────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
doc └──────────────┘
768 (Sup s) a = (⨆f∈s, (f : Πa, β a) a) :=
id └─┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └─┘ ┴ ┴
769 by rw [← Sup_image]; refl
id └───────┘
src └────┘└───────┘┴ └────
typ └────┘└───────┘┴ └────
doc └────┘ ┴ └────
txt └────┘ ┴ └────
par └────┘ ┴ └────
pid └──┘ ┴ └
st └──────────────┘┴└──────
770
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
771 lemma supr_apply {α : Type u} {β : α → Type v} {ι : Sort*} [∀ i, complete_lattice (β i)]
id ┴ ┴ └──────────────┘ ┴ ┴
src └──────────────┘
typ ┴ ┴ └──────────────┘ ┴ ┴
doc └──────────────┘
772 {f : ι → Πa, β a} {a : α} : (⨆i, f i) a = (⨆i, f i a) :=
id ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
773 by erw [← Sup_range, Sup_apply, supr_range]
id └───────┘ └───────┘ └────────┘
src └─────┘└───────┘└┘└───────┘└┘└────────┘└─
typ └─────┘└───────┘└┘└───────┘└┘└────────┘└─
doc └─────┘ └┘ └┘ └─
txt └─────┘ └┘ └┘ └─
par └─────┘ └┘ └┘ └─
pid └──┘ └┘ └┘ ┴└
st └───────────────┘└─────────┘└──────────┘┴└
774
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
775 section complete_lattice
776 variables [preorder α] [complete_lattice β]
id └──────┘ └──────────────┘
src └──────┘ └──────────────┘
typ └──────┘ └──────────────┘
doc └──────────────┘
777
778 theorem monotone_Sup_of_monotone {s : set (α → β)} (m_s : ∀f∈s, monotone f) : monotone (Sup s) :=
id └─┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘ └─┘ ┴
src └─┘ └──────┘ └──────┘ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘ └─┘ ┴
doc └──────┘ └──────┘ └─┘
779 assume x y h, Sup_le $ assume x' ⟨f, f_in, fx_eq⟩, le_Sup_of_le ⟨f, f_in, rfl⟩ $ fx_eq ▸ m_s _ f_in h
id ┴ ┴ ┴ └────┘ └┘ ┴┴ └──┘ └───┘ └──────────┘ └─┘ ┴ └─┘ ┴
src └────┘ └──────────┘ └─┘ ┴
typ ┴ ┴ ┴ └────┘ └┘ ┴┴ └──┘ └───┘ └──────────┘ └─┘ ┴ └─┘ ┴
780
781 theorem monotone_Inf_of_monotone {s : set (α → β)} (m_s : ∀f∈s, monotone f) : monotone (Inf s) :=
id └─┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘ └─┘ ┴
src └─┘ └──────┘ └──────┘ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘ └─┘ ┴
doc └──────┘ └──────┘ └─┘
782 assume x y h, le_Inf $ assume x' ⟨f, f_in, fx_eq⟩, Inf_le_of_le ⟨f, f_in, rfl⟩ $ fx_eq ▸ m_s _ f_in h
id ┴ ┴ ┴ └────┘ └┘ ┴┴ └──┘ └───┘ └──────────┘ └─┘ ┴ └─┘ ┴
src └────┘ └──────────┘ └─┘ ┴
typ ┴ ┴ ┴ └────┘ └┘ ┴┴ └──┘ └───┘ └──────────┘ └─┘ ┴ └─┘ ┴
783
784 end complete_lattice
785
786 section ord_continuous
787 open lattice
788 variables [complete_lattice α] [complete_lattice β]
id └──────────────┘ └──────────────┘
src └──────────────┘ └──────────────┘
typ └──────────────┘ └──────────────┘
doc └──────────────┘ └──────────────┘
789
790 /-- A function `f` between complete lattices is order-continuous
791 if it preserves all suprema. -/
792 def ord_continuous (f : α → β) := ∀s : set α, f (Sup s) = (⨆i∈s, f i)
id ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴
src └─┘ └─┘ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴
doc └─┘ ┴ ┴
793
794 lemma ord_continuous_sup {f : α → β} {a₁ a₂ : α} (hf : ord_continuous f) : f (a₁ ⊔ a₂) = f a₁ ⊔ f a₂ :=
id ┴ ┴ ┴ └────────────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘
src └────────────┘ ┴ ┴ ┴
typ ┴ ┴ ┴ └────────────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘
doc └────────────┘
795 have h : f (Sup {a₁, a₂}) = (⨆i∈({a₁, a₂} : set α), f i), from hf _,
id ┴ └─┘ ┴└┘┴ └┘ ┴ ┴┴ ┴└┘┴ └┘ └─┘ ┴ ┴ ┴ ┴ └┘
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
typ ┴ └─┘ ┴└┘┴ └┘ ┴ ┴┴ ┴└┘┴ └┘ └─┘ ┴ ┴ ┴ ┴ └┘
doc └─┘ ┴ ┴
796 have h₁ : {a₁, a₂} = (insert a₂ {a₁} : set α), from rfl,
id ┴└┘┴ └┘ ┴ └────┘ └┘ ┴└┘ └─┘ ┴ └─┘
src ┴ ┴ ┴ └────┘ ┴ └─┘ └─┘
typ ┴└┘┴ └┘ ┴ └────┘ └┘ ┴└┘ └─┘ ┴ └─┘
797 begin
st └─────
798 rw [h₁, Sup_insert, Sup_singleton, sup_comm] at h,
id └┘ └────────┘ └───────────┘ └──────┘
src └──┘ └┘└────────┘└┘└───────────┘└┘└──────┘└────┘
typ └──┘└┘└┘└────────┘└┘└───────────┘└┘└──────┘└────┘
doc └──┘ └┘ └┘ └┘ └────┘
txt └──┘ └┘ └┘ └┘ └────┘
par └──┘ └┘ └┘ └┘ └────┘
pid └┘ └┘ └┘ └┘ ┴└───┘
st ───────┘└──────────┘└─────────────┘└────────┘┴└───┘└─
799 rw [h, supr_insert, supr_singleton, sup_comm]
id ┴ └─────────┘ └────────────┘ └──────┘
src └──┘ └┘└─────────┘└┘└────────────┘└┘└──────┘└┘
typ └──┘┴└┘└─────────┘└┘└────────────┘└┘└──────┘└┘
doc └──┘ └┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘ └┘
pid └┘ └┘ └┘ └┘ ┴┴
st ──────┘└───────────┘└──────────────┘└────────┘┴┴
800 end
st └─┘
801
802 lemma ord_continuous_mono {f : α → β} (hf : ord_continuous f) : monotone f :=
id ┴ ┴ └────────────┘ ┴ └──────┘ ┴
src └────────────┘ └──────┘
typ ┴ ┴ └────────────┘ ┴ └──────┘ ┴
doc └────────────┘ └──────┘
803 assume a₁ a₂ h,
id └┘ └┘ ┴
typ └┘ └┘ ┴
804 calc f a₁ ≤ f a₁ ⊔ f a₂ : le_sup_left
id ┴ └┘ ┴ └┘ ┴ ┴ └┘ └─────────┘
src ┴ └─────────┘
typ ┴ └┘ ┴ └┘ ┴ ┴ └┘ └─────────┘
805 ... = f (a₁ ⊔ a₂) : (ord_continuous_sup hf).symm
id ┴ └┘ ┴ └┘ └────────────────┘ └┘ └──┘
src ┴ └────────────────┘ └──┘
typ ┴ └┘ ┴ └┘ └────────────────┘ └┘ └──┘
806 ... = _ : by rw [sup_of_le_right h]
id └─────────────┘ ┴
src └──┘└─────────────┘┴ └─
typ └──┘└─────────────┘┴┴└─
doc └──┘ ┴ └─
txt └──┘ ┴ └─
par └──┘ ┴ └─
pid └┘ ┴ ┴└
st └────────────────────┘┴└
807
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
808 end ord_continuous
809 end lattice
810
811 namespace order_dual
812 open lattice
813 variable (α : Type*)
814
815 instance [has_Inf α] : has_Sup (order_dual α) := ⟨(Inf : set α → α)⟩
id └─────┘ ┴ └─────┘ └────────┘ ┴ └─┘ └─┘ ┴ ┴
src └─────┘ └─────┘ └────────┘ └─┘ └─┘
typ └─────┘ ┴ └─────┘ └────────┘ ┴ └─┘ └─┘ ┴ ┴
doc └─────┘ └─────┘ └────────┘ └─┘
816 instance [has_Sup α] : has_Inf (order_dual α) := ⟨(Sup : set α → α)⟩
id └─────┘ ┴ └─────┘ └────────┘ ┴ └─┘ └─┘ ┴ ┴
src └─────┘ └─────┘ └────────┘ └─┘ └─┘
typ └─────┘ ┴ └─────┘ └────────┘ ┴ └─┘ └─┘ ┴ ┴
doc └─────┘ └─────┘ └────────┘ └─┘
817
818 instance [complete_lattice α] : complete_lattice (order_dual α) :=
id └──────────────┘ ┴ └──────────────┘ └────────┘ ┴
src └──────────────┘ └──────────────┘ └────────┘
typ └──────────────┘ ┴ └──────────────┘ └────────┘ ┴
doc └──────────────┘ └──────────────┘ └────────┘
819 { le_Sup := @complete_lattice.Inf_le α _,
id └─────────────────────┘ ┴
src └─────────────────────┘
typ └─────────────────────┘ ┴
820 Sup_le := @complete_lattice.le_Inf α _,
id └─────────────────────┘ ┴
src └─────────────────────┘
typ └─────────────────────┘ ┴
821 Inf_le := @complete_lattice.le_Sup α _,
id └─────────────────────┘ ┴
src └─────────────────────┘
typ └─────────────────────┘ ┴
822 le_Inf := @complete_lattice.Sup_le α _,
id └─────────────────────┘ ┴
src └─────────────────────┘
typ └─────────────────────┘ ┴
823 .. order_dual.lattice.bounded_lattice α, ..order_dual.lattice.has_Sup α, ..order_dual.lattice.has_Inf α }
id └────────────────────────────────┘ ┴ └────────────────────────┘ ┴ └────────────────────────┘ ┴
src └────────────────────────────────┘ └────────────────────────┘ └────────────────────────┘
typ └────────────────────────────────┘ ┴ └────────────────────────┘ ┴ └────────────────────────┘ ┴
824
825 instance [complete_linear_order α] : complete_linear_order (order_dual α) :=
id └───────────────────┘ ┴ └───────────────────┘ └────────┘ ┴
src └───────────────────┘ └───────────────────┘ └────────┘
typ └───────────────────┘ ┴ └───────────────────┘ └────────┘ ┴
doc └───────────────────┘ └───────────────────┘ └────────┘
826 { .. order_dual.lattice.complete_lattice α, .. order_dual.decidable_linear_order α }
id └─────────────────────────────────┘ ┴ └───────────────────────────────┘ ┴
src └─────────────────────────────────┘ └───────────────────────────────┘
typ └─────────────────────────────────┘ ┴ └───────────────────────────────┘ ┴
827
828 end order_dual
829
830 namespace prod
831 open lattice
832 variables (α : Type*) (β : Type*)
833
834 instance [has_Inf α] [has_Inf β] : has_Inf (α × β) :=
id └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
src └─────┘ └─────┘ └─────┘ ┴
typ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └─────┘ └─────┘
835 ⟨λs, (Inf (prod.fst '' s), Inf (prod.snd '' s))⟩
id ┴ ┴└─┘ └──────┘ └┘ ┴ └─┘ └──────┘ └┘ ┴
src ┴└─┘ └──────┘ └┘ └─┘ └──────┘ └┘
typ ┴ ┴└─┘ └──────┘ └┘ ┴ └─┘ └──────┘ └┘ ┴
doc └─┘ └─┘
836
837 instance [has_Sup α] [has_Sup β] : has_Sup (α × β) :=
id └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
src └─────┘ └─────┘ └─────┘ ┴
typ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └─────┘ └─────┘
838 ⟨λs, (Sup (prod.fst '' s), Sup (prod.snd '' s))⟩
id ┴ ┴└─┘ └──────┘ └┘ ┴ └─┘ └──────┘ └┘ ┴
src ┴└─┘ └──────┘ └┘ └─┘ └──────┘ └┘
typ ┴ ┴└─┘ └──────┘ └┘ ┴ └─┘ └──────┘ └┘ ┴
doc └─┘ └─┘
839
840 instance [complete_lattice α] [complete_lattice β] : complete_lattice (α × β) :=
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ ┴ ┴
src └──────────────┘ └──────────────┘ └──────────────┘ ┴
typ └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴ ┴ ┴
doc └──────────────┘ └──────────────┘ └──────────────┘
841 { le_Sup := assume s p hab, ⟨le_Sup $ mem_image_of_mem _ hab, le_Sup $ mem_image_of_mem _ hab⟩,
id ┴ ┴ └─┘ └────┘ └──────────────┘ └─┘ └────┘ └──────────────┘ └─┘
src └────┘ └──────────────┘ └────┘ └──────────────┘
typ ┴ ┴ └─┘ └────┘ └──────────────┘ └─┘ └────┘ └──────────────┘ └─┘
842 Sup_le := assume s p h,
id ┴ ┴ ┴
typ ┴ ┴ ┴
843 ⟨ Sup_le $ ball_image_of_ball $ assume p hp, (h p hp).1,
id └────┘ └────────────────┘ ┴ └┘ ┴ ┴ └┘ ┴
src └────┘ └────────────────┘ ┴
typ └────┘ └────────────────┘ ┴ └┘ ┴ ┴ └┘ ┴
844 Sup_le $ ball_image_of_ball $ assume p hp, (h p hp).2⟩,
id └────┘ └────────────────┘ ┴ └┘ ┴ ┴ └┘ ┴
src └────┘ └────────────────┘ ┴
typ └────┘ └────────────────┘ ┴ └┘ ┴ ┴ └┘ ┴
845 Inf_le := assume s p hab, ⟨Inf_le $ mem_image_of_mem _ hab, Inf_le $ mem_image_of_mem _ hab⟩,
id ┴ ┴ └─┘ └────┘ └──────────────┘ └─┘ └────┘ └──────────────┘ └─┘
src └────┘ └──────────────┘ └────┘ └──────────────┘
typ ┴ ┴ └─┘ └────┘ └──────────────┘ └─┘ └────┘ └──────────────┘ └─┘
846 le_Inf := assume s p h,
id ┴ ┴ ┴
typ ┴ ┴ ┴
847 ⟨ le_Inf $ ball_image_of_ball $ assume p hp, (h p hp).1,
id └────┘ └────────────────┘ ┴ └┘ ┴ ┴ └┘ ┴
src └────┘ └────────────────┘ ┴
typ └────┘ └────────────────┘ ┴ └┘ ┴ ┴ └┘ ┴
848 le_Inf $ ball_image_of_ball $ assume p hp, (h p hp).2⟩,
id └────┘ └────────────────┘ ┴ └┘ ┴ ┴ └┘ ┴
src └────┘ └────────────────┘ ┴
typ └────┘ └────────────────┘ ┴ └┘ ┴ ┴ └┘ ┴
849 .. prod.lattice.bounded_lattice α β,
id └──────────────────────────┘ ┴ ┴
src └──────────────────────────┘
typ └──────────────────────────┘ ┴ ┴
850 .. prod.lattice.has_Sup α β,
id └──────────────────┘ ┴ ┴
src └──────────────────┘
typ └──────────────────┘ ┴ ┴
851 .. prod.lattice.has_Inf α β }
id └──────────────────┘ ┴ ┴
src └──────────────────┘
typ └──────────────────┘ ┴ ┴
852
853 end prod